A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family

DOI10.1007/978-3-540-74464-1_7zbMath1178.03026OpenAlexW1548537769MaRDI QIDQ3612438

Nils Anders Danielsson

Publication date: 10 March 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74464-1_7

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (8)

Strongly typed term representations in Coq ⋮ Normalization by evaluation for modal dependent type theory ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Pure type systems with explicit substitutions ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Type Theory Should Eat Itself ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction

This page was built for publication: A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family