scientific article; zbMATH DE number 6744143

DOI10.4230/LIPICS.TLCA.2015.31MaRDI QIDQ5277828zbMATHFDO

Authors Maen Al Assaf

Publication date 12 July 2017

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

zbMATH Keywords

normalizationconservativitylogical frameworkpure type systems\(\lambda \Pi\) calculus modulo rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Extending Abramsky's lazy lambda calculus: (non)-conservativity of embeddings
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• scientific article; zbMATH DE number 445155
• scientific article; zbMATH DE number 2174387
• Consistency and Completeness of Rewriting in the Calculus of Constructions
• Consistency and Completeness of Rewriting in the Calculus of Constructions
• Preservation of strong normalisation modulo permutations for the structural \(\lambda\)-calculus
• Conservation and uniform normalization in lambda calculi with erasing reductions
• scientific article; zbMATH DE number 7204561
• On modular properties of higher order extensional lambda calculi

Cited in

(5)

• Objects and subtyping in the \(\lambda\)-\(\Pi\)-calculus modulo
• On the conservativity of Leibniz equality
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Extending Abramsky's lazy lambda calculus: (non)-conservativity of embeddings

This page was built for publication:

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