Equivalences between pure type systems and systems of illative combinatory logic

DOI10.1305/NDJFL/1117755149zbMath1081.03015OpenAlexW2019024348MaRDI QIDQ2565990

Martin W. Bunder, Wil Dekkers

Publication date: 28 September 2005

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1117755149

zbMATH Keywords

pure type systemsillative combinatory logic

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (2)

Variants of the basic calculus of constructions ⋮ Higher-Order Illative Combinatory Logic

Uses Software

• APTS
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Possible forms of evaluation or reduction in Martin-Löf type theory
• On the equivalence of systems of rules and systems of axioms in illative combinatory logic
• A deduction theorem for restricted generality
• Combinatory logic. Vol. II
• Equality in 𝔉 with Restricted Subjects
• Consistency notions in illative combinatory logic
• On the inconsistency of systems similar to
• Pure type systems with more liberal rules
• Some consistency proofs and a characterization of inconsistency proofs in illative combinatory logic
• Propositional and predicate calculus based on combinatory logic
• Various systems of set theory based on combinatory logic
• On the proof theory of Coquand's calculus of constructions

This page was built for publication: Equivalences between pure type systems and systems of illative combinatory logic