Implementing a normalizer using sized heterogeneous types
From MaRDI portal
Publication:3638918
DOI10.1017/S0956796809007266zbMath1191.68152MaRDI QIDQ3638918
Publication date: 28 October 2009
Published in: Journal of Functional Programming (Search for Journal in Brave)
Related Items (3)
Cites Work
- Unnamed Item
- Substitution: A formal methods case study using monads and transformations
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- Inductive types and type constraints in the second-order lambda calculus
- de Bruijn notation as a nested datatype
- Type-based termination of recursive definitions
- Termination checking with types
- Mechanizing metatheory in a logical framework
- Intensional interpretations of functionals of finite type I
This page was built for publication: Implementing a normalizer using sized heterogeneous types