Zobrazeno 1 - 10
of 14
pro vyhledávání: '"ACM: F.3.2"'
Autor:
Joachim De Lataillade
Publikováno v:
Mathematical Structures in Computer Science. 18:647-692
Curry-style system F, ie. system F with no explicit types in terms, can be seen as a core presentation of polymorphism from the point of view of programming languages. This paper gives a characterisation of type isomorphisms for this language, by usi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3834790038f08acc0fa34604ba19fa94
https://doi.org/10.1017/s0960129508006828
https://doi.org/10.1017/s0960129508006828
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⟩
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
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⟩
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
Autor:
Olivier Laurent
Publikováno v:
Logical Methods in Computer Science
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2010, 6 (4), pp.3. ⟨10.2168/LMCS-6(4:3)2010⟩
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2010, 6 (4), pp.3. ⟨10.2168/LMCS-6(4:3)2010⟩
International audience; We refine HO/N game semantics with an additional notion of pointer (mu-pointers) and extend it to first-order classical logic with completeness results. We use a Church style extension of Parigot's lambda-mu-calculus to repres
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::37b40ca69b44edcabaaa325a95ef9847
https://hal.archives-ouvertes.fr/hal-00528528
https://hal.archives-ouvertes.fr/hal-00528528
Autor:
Olivier Laurent, Thomas Ehrhard
Publikováno v:
Logical Methods in Computer Science
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2010, 6 (3), pp.11. ⟨10.2168/LMCS-6(3:11)2010⟩
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2010, 6 (3), pp.11. ⟨10.2168/LMCS-6(3:11)2010⟩
International audience; We present a restriction of the solos calculus which is stable under reduction and expressive enough to contain an encoding of the pi-calculus. As a consequence, it is shown that equalizing names that are already equal is not
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e980787a3d41d66f37a832c3e0f86cbf
https://hal.archives-ouvertes.fr/hal-00516609
https://hal.archives-ouvertes.fr/hal-00516609
Autor:
Thomas Ehrhard, Olivier Laurent
Publikováno v:
Information and Computation
Information and Computation, Elsevier, 2010, 208 (6), pp.606--633. ⟨10.1016/j.ic.2009.06.005⟩
CONCUR 2007 – Concurrency Theory
CONCUR 2007
CONCUR 2007, Sep 2007, Lisboa, Portugal. pp.333-348, ⟨10.1007/978-3-540-74407-8⟩
Information and Computation, 2010, 208 (6), pp.606--633. ⟨10.1016/j.ic.2009.06.005⟩
CONCUR 2007 – Concurrency Theory ISBN: 9783540744061
CONCUR
Information and Computation, Elsevier, 2010, 208 (6), pp.606--633. ⟨10.1016/j.ic.2009.06.005⟩
CONCUR 2007 – Concurrency Theory
CONCUR 2007
CONCUR 2007, Sep 2007, Lisboa, Portugal. pp.333-348, ⟨10.1007/978-3-540-74407-8⟩
Information and Computation, 2010, 208 (6), pp.606--633. ⟨10.1016/j.ic.2009.06.005⟩
CONCUR 2007 – Concurrency Theory ISBN: 9783540744061
CONCUR
International audience; We propose and study a translation of a pi-calculus without sums nor recursion into an untyped version of differential interaction nets. We define a transition system of labeled processes and a transition system of labeled dif
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a4e8f3f1f3b7b972db480d5dd7495ef7
https://hal.archives-ouvertes.fr/hal-00483780
https://hal.archives-ouvertes.fr/hal-00483780
Autor:
Bernard, Noël, Dumond, Yves
Submitted to publication; In this paper, we bring in a dialect of the pi-calculus which involves explicit substitutions. This mechanism has the property to handle substitutions in such a way that it avoids deep parsing of the terms concerned. Then, w
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::29fdd97f03e9252673182fd103bb25e9
https://hal.archives-ouvertes.fr/hal-00387065
https://hal.archives-ouvertes.fr/hal-00387065
Autor:
Danos, Vincent, Ehrhard, Thomas
29 pages; We introduce a probabilistic version of coherence spaces and show that these objects provide a model of linear logic. We build a model of the pure lambda-calculus in this setting and show how to interpret a probabilistic version of the func
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::009be5bd5a743519be4d80662cc96dd6
https://hal.archives-ouvertes.fr/hal-00280462/document
https://hal.archives-ouvertes.fr/hal-00280462/document
Publikováno v:
Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings
Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL
Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Sep 2007, Lausanne, Switzerland. pp.298-312
Computer Science Logic ISBN: 9783540749141
CSL
Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL
Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Sep 2007, Lausanne, Switzerland. pp.298-312
Computer Science Logic ISBN: 9783540749141
CSL
Models of the untyped λ-calculus may be defined either as applicative structures satisfying a bunch of first-order axioms (λ-models), or as reflexive objects in cartesian closed categories (categorical models). In this paper we show that any catego
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7515ed0fdf23c9a4dc60deedf77c938f
https://hal.archives-ouvertes.fr/hal-00148820/file/enough.pdf
https://hal.archives-ouvertes.fr/hal-00148820/file/enough.pdf
Autor:
Radhia Cousot, Patrick Cousot, David Monniaux, Antoine Miné, Jérôme Feret, Laurent Mauborgne, Xavier Rival
Publikováno v:
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007. TASE '07
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), Jun 2007, Shanghai, China. pp.3-20, ⟨10.1109/TASE.2007.55⟩
TASE
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), Jun 2007, Shanghai, China. pp.3-20, ⟨10.1109/TASE.2007.55⟩
TASE
We discuss the characteristic properties of ASTRÉE, an automatic static analyzer for proving the absence of runtime errors in safety-critical real-time synchronous control/command C programs, and compare it with a variety of other program analysis t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::aedce464cb9009914f13db89d9f522a6
https://hal.archives-ouvertes.fr/hal-00154031/document
https://hal.archives-ouvertes.fr/hal-00154031/document