An extended type system with lambda-typed lambda-expressions

MaRDI QIDQ5140267zbMATH OpenFDO

Authors

Publication date 15 December 2020

Full work available at URL https://arxiv.org/abs/1803.10143, https://lmcs.episciences.org/6946

zbMATH Keywords

higher-order logicstrong normalizationtyped lambda calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• The formal system λδ
• scientific article; zbMATH DE number 512879
• Introduction to generalized type systems
• Some lambda calculus and type theory formalized
• scientific article; zbMATH DE number 1678362

Cites work

• PAL⁺: a lambda-free logical framework
• A formulation of the simple theory of types
• A symmetric lambda calculus for classical program extraction
• Explicit substitutions
• Formulae-as-types for an involutive negation
• scientific article; zbMATH DE number 1670497 (Why is no real title available?)
• scientific article; zbMATH DE number 2185666 (Why is no real title available?)
• scientific article; zbMATH DE number 4191621 (Why is no real title available?)
• scientific article; zbMATH DE number 4058907 (Why is no real title available?)
• scientific article; zbMATH DE number 3657156 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 65528 (Why is no real title available?)
• scientific article; zbMATH DE number 512879 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• On -conversion in the -cube and the combination with abbreviations
• On theories with a combinatorial definition of 'equivalence'
• The duality of computation
• The formal system λδ
• The foundation of a generic theorem prover
• The structural \(\lambda \)-calculus
• Typed \lambda-calculi with one binder

Cited in

(2)

• System F-omega with equirecursive types for datatype-generic programming
• Extension of the formal system of the theory of expressions with arities and its strong normalization property

Describes a project that uses

Uses Software

• Automath

This page was built for publication: An extended type system with lambda-typed lambda-expressions

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