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 archivesActive forum topics
New forum topics

Recent comments
1 day 6 hours ago
1 day 16 hours ago
2 days 2 hours ago
2 days 5 hours ago
2 days 5 hours ago
2 days 9 hours ago
2 days 13 hours ago
2 days 13 hours ago
2 days 18 hours ago
2 days 18 hours ago