Interactive models of computation and program behavior / Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine... [et al.]

Auteur: Curien, Pierre-Louis (1953-) - AuteurCo-auteur: Herbelin, Hugo - Auteur ; Krivine, Jean-Louis (1939-) - AuteurType de document: MonographieCollection: Panoramas et synthèses ; 27Langue: anglaisPays: FranceÉditeur: Paris : Société Mathématique de France, 2009Description: 1 vol. (XVI-275 p.) : fig. ; 24 cm ISBN: 9782856292730 ; br. Résumé: From the abstract: “This volume contains three contributions in the field of logic and computation that reflect current trends towards an interactive account of the meaning of proofs and programs. The contributions can be read independently and use or introduce fundamental tools in the field: categories, realizability, abstract machines. Throughout the volume, a unifying theme is that of games and strategies, that turns the correspondence between proofs and programs (the so-called Curry-Howard isomorphism) into a triangle whose third corner emphasizes interaction and duality between a program and its environement or between a proof and counter-proofs. The introduction to the volume places the contributions in perspective and provides a gentle beginner's introduction to the lambda-calculus, which is and remains the backbone of the whole field.".Bibliographie: Références bibliogr. en fin de contributions. Sujets MSC: 03B70 Mathematical logic and foundations -- General logic -- Logic in computer science
03B40 Mathematical logic and foundations -- General logic -- Combinatory logic and lambda-calculus
03F52 Mathematical logic and foundations -- Proof theory and constructive mathematics -- Linear logic and other substructural logics
03G30 Mathematical logic and foundations -- Algebraic logic -- Categorical logic, topoi
18C50 Category theory; homological algebra -- Categories and theories -- Categorical semantics of formal languages
68N18 Computer science -- Software -- Functional programming and lambda calculus
En-ligne: Sommaire
Location Call Number Status Date Due
Couloir 07250-01 / Séries Panor 27 (Browse Shelf) Available

Références bibliogr. en fin de contributions

From the abstract: “This volume contains three contributions in the field of logic and computation that reflect current trends towards an interactive account of the meaning of proofs and programs. The contributions can be read independently and use or introduce fundamental tools in the field: categories, realizability, abstract machines. Throughout the volume, a unifying theme is that of games and strategies, that turns the correspondence between proofs and programs (the so-called Curry-Howard isomorphism) into a triangle whose third corner emphasizes interaction and duality between a program and its environement or between a proof and counter-proofs. The introduction to the volume places the contributions in perspective and provides a gentle beginner's introduction to the lambda-calculus, which is and remains the backbone of the whole field."

There are no comments for this item.

Log in to your account to post a comment.
Languages: English | Français | |