Stephan Herhut

I will be giving a presentation at this year’s International Symposium on Implementation and Application of Functional Language. The paper is titled From Contracts Towards Dependent Types: Proofs by Partial Evaluation. The idea is to use explicit contracts to express domain constraints, etc. and to use existing partial evaluation techniques to prove as many of these constraints at compile time as possible. Thus, you gain the static safety of dependent types where possible and retain the flexibility of weaker typed languages where needed.