Publication:4297779

zbMath0842.03023MaRDI QIDQ4297779

Jean-Louis Krivine

Publication date: 2 December 1995

zbMATH Keywords

survey; proof theory; \(\lambda\)-calculus; functional programming; Curry-Howard isomorphism; programming theory; concealed programming meaning of mathematical theorems; functions and proofs as programs; theorems as specifications

Mathematics Subject Classification ID

68-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science

00A30: Philosophy of mathematics

03-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

03B40: Combinatory logic and lambda calculus

Related Items

From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models