## User login## Navigation |
## Dependently Typed Programming based on Automated Theorem Proving
Coq and Agda are demonstrating the dependently-typed 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 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 type-checker for a dependently-typed language needs to be convinced of the validity of some user code. So there is a non-trivial engineering issue to be solved regarding the implementation of a |
## Browse archives## Active forum topics- Looking for references on the expressiveness and computational completeness of a relational programming language
- language handling of memory and other resource failures
- Whither FRP?
- Programming Languages as Mathematical Representations
- Is there a language with the ability to write arbitrary type functions?
## New forum topics |

## Recent comments

2 hours 8 min ago

3 hours 53 min ago

5 hours 9 min ago

10 hours 22 min ago

17 hours 36 min ago

19 hours 54 min ago

21 hours 11 min ago

21 hours 57 min ago

23 hours 16 min ago

23 hours 21 min ago