Hereditary substitution for the -calculus

zbMATH Open1471.03023arXiv1309.1256MaRDI QIDQ4957789FDOQ4957789

Authors:

Publication date: 9 September 2021

Full work available at URL: https://arxiv.org/abs/1309.1256

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

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)

Cites Work

• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Types for Proofs and Programs
• Finitely stratified polymorphism
• Proofs of strong normalisation for second order classical natural deduction
• Title not available (Why is that?)
• Types for Proofs and Programs
• Weak normalization implies strong normalization in a class of non-dependent pure type systems
• Implementing a normalizer using sized heterogeneous types
• Syntactic Metatheory of Higher-Order Subtyping

Cited In (3)

• Graded modal dependent type theory
• Title not available (Why is that?)
• Implementing a normalizer using sized heterogeneous types

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)