First order marked types

DOI10.1007/3-540-61780-9_65zbMath1434.03027OpenAlexW1497865772MaRDI QIDQ4647574

Philippe Curmin

Publication date: 15 January 2019

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

Full work available at URL: https://doi.org/10.1007/3-540-61780-9_65

zbMATH Keywords

natural deductionelimination ruleexistential quantifierclosed termmarked version

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Cites Work

• Unnamed Item
• Unnamed Item
• Extraction of redundancy-free programs from constructive natural deduction proofs
• Pruning simply typed  -terms

This page was built for publication: First order marked types