Hereditary substitution for the -calculus

MaRDI QIDQ4957789zbMATH OpenFDO

Authors

Publication date 9 September 2021

Full work available at URL https://arxiv.org/abs/1309.1256, http://eptcs.web.cse.unsw.edu.au/paper.cgi?COS2013.4

Mathematics Subject Classification ID

Type theory (03B38) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Functional programming and lambda calculus (68N18)

Recommendations

• Implementing a normalizer using sized heterogeneous types
• Functional and Logic Programming
• scientific article; zbMATH DE number 1088029
• Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi
• Strong normalization of substitutions

Cites work

• An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
• Finitely stratified polymorphism
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 1229489 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 1479632 (Why is no real title available?)
• Implementing a normalizer using sized heterogeneous types
• Proofs of strong normalisation for second order classical natural deduction
• Syntactic Metatheory of Higher-Order Subtyping
• Types for Proofs and Programs
• Types for Proofs and Programs
• Weak normalization implies strong normalization in a class of non-dependent pure type systems

Cited in

(3)

• Graded modal dependent type theory
• Implementing a normalizer using sized heterogeneous types
• scientific article; zbMATH DE number 1088029 (Why is no real title available?)

This page was built for publication: Hereditary substitution for the \(\lambda \Delta \)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4957789)