Publication:3564946

zbMath1205.03045MaRDI QIDQ3564946

Pierre-Louis Curien, Paul-André Melliès, Hugo Herbelin, Jean-Louis Krivine

Publication date: 27 May 2010

zbMATH Keywords

linear logic; proof theory; realizability; categorical models; game semantics; Curry-Howard correspondence; abstract machines

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

03G30: Categorical logic, topoi

68-02: Research exposition (monographs, survey articles) pertaining to computer science

18C50: Categorical semantics of formal languages

03F52: Proof-theoretic aspects of linear logic and other substructural logics

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

03B40: Combinatory logic and lambda calculus

Related Items

POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, The parametric continuation monad, Non-linearity as the Metric Completion of Linearity, Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language, Resource modalities in tensor logic, Ordered combinatory algebras and realizability