Are there Hilbert-style Pure Type Systems?

DOI10.2168/LMCS-4(1:1)2008MaRDI QIDQ3518266zbMATH OpenOpenAlexFDO

Authors Wil Dekkers, Martin W. Bunder

Publication date 7 August 2008

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/lmcs-4(1:1)2008

zbMATH Keywords

Hilbert-style logicillative combinatory logiclambda calculuspure type system

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Recommendations

• Equivalences between pure type systems and systems of illative combinatory logic
• scientific article; zbMATH DE number 1377703
• Pure type system conversion is always typable
• Pure type systems with more liberal rules
• Typing in pure type systems

Cited in

(1)

• scientific article; zbMATH DE number 1377703 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Are there Hilbert-style Pure Type Systems?

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