The formal system λδ

DOI10.1145/1614431.1614436zbMATH Open1351.68059OpenAlexW2012542922MaRDI QIDQ2946591FDOQ2946591

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

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}^*\)

zbMATH Keywords

abbreviationsenvironments as termsterms as types

Mathematics Subject Classification ID

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

Cited In (9)

• A minimalist two-level foundation for constructive mathematics
• Title not available (Why is that?)
• A unified approach to type theory through a refined \(\lambda\)-calculus
• Verified representations of Landau's ``Grundlagen in the \(\lambda\delta\) family and in the calculus of constructions
• 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^*\)
• 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

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)