User loginNavigation 
Dependently Typed Programming based on Automated Theorem ProvingDependently Typed Programming based on Automated Theorem Proving, by Alasdair Armstrong, Simon Foster, and Georg Struth. [Link to preprint on ArXiv, a.k.a. this has not yet been refereed, use at your own risk].
Coq and Agda are demonstrating the dependentlytyped programming is feasible and beneficial  but still quite painful in practice. The point of computers is that they can automate a lot of drudgery. And a lot of proofs ought to be considered drudgery as well. But, in practice, this is a huge leap. The authors present an interesting experiment in a promising direction. The LtU angle here is that current (automated) proof assistants generate proofs which, usually, have a huge impedance mismatch with the kinds of evidence that a typechecker for a dependentlytyped language needs to be convinced of the validity of some user code. So there is a nontrivial engineering issue to be solved regarding the implementation of a pleasant environment for dependentlytyped programming. 
Browse archives
Active forum topics

Recent comments
49 min 25 sec ago
2 hours 33 min ago
2 hours 38 min ago
2 hours 55 min ago
2 hours 58 min ago
7 hours 14 min ago
10 hours 47 min ago
11 hours 27 min ago
11 hours 28 min ago
11 hours 39 min ago