The formal system λδ

DOI10.1145/1614431.1614436MaRDI QIDQ2946591zbMATHOpenAlexFDO

Authors Ferruccio Guidi

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1614431.1614436

zbMATH Keywords

abbreviationsenvironments as termsterms as types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Publication:4490747
• An extension of the formal deductive system \({\mathcal L}^*\)
• Type system \(\lambda\omega\times_\leqq\)
• A kind of simplified formal deductive system \(L_0^*\) for the system \(L^*\)
• The completeness of the formal deductive system \(\mathcal{L}^*(n)\)
• scientific article; zbMATH DE number 1780077
• The structural \(\lambda \)-calculus
• THE Σλ-CALCULUS AND DERIVED PROGRAM FORMS
• Calculus CL as a Formal System
• A kind of improved formal deductive system \(\mathcal{L}_0^*\) for the system \(\mathcal{L}^*\)

Cited in

(9)

• Verified representations of Landau's ``Grundlagen in the \(\lambda\delta\) family and in the calculus of constructions
• A necessary and sufficient condition for the uniqueness of \(\beta\delta\)-normal form of typed \(\lambda\)-terms for the canonical notion of \(\delta\)-reduction
• A Formal System for the Universal Quantification of Schematic Variables
• An extended type system with lambda-typed lambda-expressions
• Procedural representation of CIC proof terms
• A kind of simplified formal deductive system \(L_0^*\) for the system \(L^*\)
• scientific article; zbMATH DE number 1943083 (Why is no real title available?)
• A unified approach to type theory through a refined \(\lambda\)-calculus
• A minimalist two-level foundation for constructive mathematics

This page was built for publication: The formal system λδ

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