Conservativity between logics and typed λ calculi

DOI10.1007/3-540-58085-9_73zbMath1527.03012MaRDI QIDQ6083691

Herman Geuvers

Publication date: 8 December 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://repository.ubn.ru.nl//bitstream/handle/2066/104050/104050.pdf

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Constructivism in mathematics. An introduction. Volume II
• On the adequacy of representing higher order intuitionistic logic as a pure type system
• Constructive natural deduction and its ‘ω-set’ interpretation
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• Embedding first order predicate logic in fragments of intuitionistic logic