An induction principle for pure type systems

DOI10.1016/S0304-3975(00)00373-XzbMath0992.68188OpenAlexW1982157045MaRDI QIDQ5958776

Morten Heine B. Sørensen, Gilles Barthe, John Hatcliff

Publication date: 3 March 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00373-x

zbMATH Keywords

pure type systemsinduction principle

Mathematics Subject Classification ID

Uses Software

• Automath
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The calculus of constructions
• CPS translations and applications: The cube and beyond
• On multiset orderings
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Strong normalization in type systems: A model theoretical approach
• A framework for defining logics
• Expansion postponement for normalising pure type systems
• Domain-free pure type systems
• A-translation and looping combinators in pure type systems
• Introduction to generalized type systems
• Type-checking injective pure type systems
• Weak normalization implies strong normalization in a class of non-dependent pure type systems