Formal polytypic programs and proofs
From MaRDI portal
Publication:3070767
DOI10.1017/S0956796810000158zbMath1208.68106MaRDI QIDQ3070767
Edsko Devries, Wendy Verbruggen, Arthur Hughes
Publication date: 26 January 2011
Published in: Journal of Functional Programming (Search for Journal in Brave)
Uses Software
Cites Work
- Type-based termination of generic programs
- Generic programming in 3D
- Type checking with universes
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Inductive and Coinductive Components of Corecursive Functions in Coq
- Complete and decidable type inference for GADTs
- A UNIVERSE OF STRICTLY POSITIVE FAMILIES
- Container types categorically
- Derivable Type Classes
- Generics for the masses
- Boxy types