scientific article; zbMATH DE number 1354162

MaRDI QIDQ4268477zbMATH OpenFDO

Authors Michel Parigot

Publication date 28 October 1999

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cited in

(13)

• Recursive programming with proofs
• The Inf function in the system \(F\)
• From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
• Strong storage operators and data types
• Minimality in a linear calculus with iteration
• Efficient lambda encodings for Mendler-style coinductive types in Cedille
• Monotone recursive types and recursive data representations in Cedille
• Some remarks on type systems for course-of-value recursion
• A Tutorial on Type-Based Termination
• Efficiency of lambda-encodings in total type theory
• The calculus of dependent lambda eliminations
• Impredicative encodings of inductive-inductive data in Cedille
• On the confluence of lambda-calculus with conditional rewriting

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 Q4268477)