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

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

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

• 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?)
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Finitely stratified polymorphism
• 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)