Pure type systems with explicit substitutions

DOI10.1017/S0956796815000210zbMath1420.68038MaRDI QIDQ5371956

Daniel Fridlender, Miguel Pagano

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796815000210

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03B40: Combinatory logic and lambda calculus

Uses Software

• Coq
• Matita
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Pure type systems with explicit substitution
• Dependent types and explicit substitutions: a meta-theoretical development
• Pure Type System conversion is always typable
• A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Remarks on the equational theory of non-normalizing pure type systems
• Pure type systems with judgemental equality
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• Towards Normalization by Evaluation for the βη-Calculus of Constructions
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• Big-step normalisation
• Confluence properties of weak and strong calculi of explicit substitutions
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Internal type theory
• Domain-free pure type systems
• Strong normalization of substitutions
• The Matita Interactive Theorem Prover
• A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation