A refined interpretation of intuitionistic logic by means of atomic polymorphism

DOI10.1007/s11225-019-09858-1zbMath1479.03006MaRDI QIDQ2186692

Gilda Ferreira, José Espírito Santo

Publication date: 9 June 2020

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1822/73100

zbMATH Keywords

permutative conversion; atomic system F; instantiation overflow

Mathematics Subject Classification ID

03F07: Structure of proofs

03F03: Proof theory in general (including proof-theoretic semantics)

03B20: Subsystems of classical logic (including intuitionistic logic)

03B40: Combinatory logic and lambda calculus

03B38: Type theory