A Tutorial on Type-Based Termination
From MaRDI portal
Publication:5191089
DOI10.1007/978-3-642-03153-3_3zbMath1250.68084OpenAlexW1661875115MaRDI QIDQ5191089
Benjamin Grégoire, Gilles Barthe, Colin Riba
Publication date: 28 July 2009
Published in: Language Engineering and Rigorous Software Development (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-03153-3_3
Related Items
A sound strategy to compile general recursion into finite depth pattern matching ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ Partiality and recursion in interactive theorem provers – an overview
Cites Work
- What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
- Higher-order subtyping
- Dependent types for program termination verification
- Type fixpoints
- Type-based termination of recursive definitions
- Termination checking with types
- Typed Lambda Calculi and Applications
- Semi-continuous Sized Types and Termination
- Calculating sized types
- Unnamed Item
- Unnamed Item
- Unnamed Item
