Výsledky vyhledávání - "Laurent Regnier"

Elektronická kniha

Autor: Jean-Yves Girard, Yves Lafont, Laurent Regnier

Linear logic, introduced in 1986 by J.-Y. Girard, is based upon a fine grain analysis of the main proof-theoretical notions of logic. The subject develops along the lines of denotational semantics, proof nets and the geometry of interaction. Its basi

Zobrazit plný text záznamu

Differential interaction nets

Autor: Thomas Ehrhard, Laurent Regnier

Publikováno v: Theoretical Computer Science
Theoretical Computer Science, Elsevier, 2006, 364 (2), pp.166-195. ⟨10.1016/j.tcs.2006.08.003⟩
Theoretical Computer Science, 2006, 364 (2), pp.166-195. ⟨10.1016/j.tcs.2006.08.003⟩

30 pages; International audience; We introduce interaction nets for a fragment of the differential lambda-calculus and exhibit in this framework a new symmetry between the "of course" and the "why not" modalities of linear logic, which is completely

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ff1d7c06ccd47f3efc7b4fbb87999f3f

Zobrazit plný text záznamu

The differential lambda-calculus

Autor: Laurent Regnier, Thomas Ehrhard

Publikováno v: Theoretical Computer Science
Theoretical Computer Science, 2003, 309 (1-3), pp.1-41. ⟨10.1016/S0304-3975(03)00392-X⟩
Theoretical Computer Science, Elsevier, 2003, 309 (1-3), pp.1-41. ⟨10.1016/S0304-3975(03)00392-X⟩

41 pages; International audience; We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bb64d932bd9701b8ef09b96c380f95a2

Zobrazit plný text záznamu

Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms

Autor: Thomas Ehrhard, Laurent Regnier

Publikováno v: Logical Approaches to Computational Barriers ISBN: 9783540354666
CiE

We introduce and study a version of Krivine's machine which provides a precise information about how much of its argument is needed for performing a computation. This information is expressed as a term of a resource lambda-calculus introduced by the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::22da0c66eef80738c2e093219953f14b
https://doi.org/10.1007/11780342_20

Zobrazit plný text záznamu

About Translations of Classical Logic into Polarized Linear Logic

Autor: O. Laurent, Laurent Regnier

Publikováno v: Logic in Computer Science
LICS

We show that the decomposition of intuitionistic logic into linear logic along the equation A /spl rarr/ B = !A /spl rarr/ B may be adapted into a decomposition of classical logic into LLP, the polarized version of Linear Logic. Firstly, we build a c

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d22ddda982dc999307344a60a3b2dfde
https://hal.archives-ouvertes.fr/hal-00009139

Zobrazit plný text záznamu

Local and asynchronous beta-reduction (an analysis of Girard's execution formula)

Autor: Laurent Regnier, Vincent Danos

Publikováno v: LICS

The authors build a confluent, local, asynchronous reduction on lambda -terms, using infinite objects (partial injections of Girard's (1988) algebra L*), which is simple (only one move), intelligible (semantic setting of the reduction), and general (

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::93a7091fcf68ae0fd545517ec251759d
https://doi.org/10.1109/lics.1993.287578

Zobrazit plný text záznamu

Game semantics and abstract machines

Autor: Hugo Herbelin, Vincent Danos, Laurent Regnier

Publikováno v: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science.

The interaction processes at work by M. Hyland and L. Ong (1994) (HO) and S. Abramsky et al. (1994) (AJM) new game semantics are two preexisting paradigmatic implementations of linear head reduction: respectively Krivine's abstract machine and Girard

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::2a70bce177cdb9957b396d7764e441fb
https://doi.org/10.1109/lics.1996.561456

Zobrazit plný text záznamu

Paths in the lambda-calculus. Three years of communications without understanding

Autor: Vincent Danos, Cosimo Laneve, Laurent Regnier, Andrea Asperti

Publikováno v: Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science.

Since the rebirth of /spl lambda/-calculus in the late 1960s, three major theoretical investigations of /spl beta/-reduction have been undertaken: (1) Levy's (1978) analysis of families of redexes (and the associated concept of labeled reductions); (

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::2e3c1035fe7e4fefedc98a252e3397d6
https://doi.org/10.1109/lics.1994.316048

Zobrazit plný text záznamu

Believe it or not, AJM's Games Model is a Model of Classical Linear Logic

Autor: Patrick Baillot, Laurent Regnier, Thomas Ehrhard, Vincent Danos

Publikováno v: Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97)
LICS

A general category of games is constructed. A subcategory of saturated strategies, closed under all possible codings in copy games, is shown to model reduction in classical linear logic.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::facf88d14a63325df9f1be8d56671dbb
https://hal.science/hal-00084630

Zobrazit plný text záznamu

Directed virtual reductions

Autor: Vincent Danos, Laurent Regnier, Marco Pedicini

Publikováno v: Computer Science Logic ISBN: 9783540631729
CSL

This note defines a new graphical local calculus, directed virtual reductions. It is designed to compute Girard's execution formula EX, an invariant of closed functional evaluation obtained from the “geometry of interaction” interpretation of λ-

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9404cdfbeb969cbc7827bef105142d90
https://doi.org/10.1007/3-540-63172-0_33

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání