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
8 hours 35 min ago
8 hours 46 min ago
1 day 14 hours ago
6 days 21 hours ago
1 week 1 day ago
2 weeks 5 days ago
3 weeks 4 days ago
4 weeks 4 days ago
6 weeks 2 days ago
6 weeks 5 days ago