Zobrazeno 1 - 10
of 22
pro vyhledávání: '"Stéphane Lengrand"'
Autor:
Stéphane Lengrand, Murdoch J. Gabbay
Publikováno v:
Information and Computation. 207:1369-1400
We present the Lambda Context Calculus. This simple lambda-calculus features variables arranged in a hierarchy of strengths such that substitution of a strong variable does not avoid capture with respect to abstraction by a weaker variable. This allo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3c6407d82c60f299743a5c4298fa042b
https://doi.org/10.1016/j.ic.2009.06.004
https://doi.org/10.1016/j.ic.2009.06.004
Autor:
Stéphane Lengrand, Alexandre Miquel
Publikováno v:
Annals of Pure and Applied Logic. 153:3-20
We present a version of system F ω , called F ω c , in which the layer of type constructors is essentially the traditional one of F ω , whereas provability of types is classical. The proof-term calculus accounting for the classical reasoning is a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5505c6a45ef534478865762682604950
https://doi.org/10.1016/j.apal.2008.01.005
https://doi.org/10.1016/j.apal.2008.01.005
Autor:
Roy Dyckhoff, Stéphane Lengrand
Publikováno v:
Journal of Logic and Computation. 17:1109-1134
LJQ is a focused sequent calculus for intuitionistic logic, with a simple restriction on the first premiss of the usual left introduction rule for implication. In a previous paper we discussed its history (going back to about 1950, or beyond) and pre
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6c5f6542d86b6ae962d224fe894b6986
https://doi.org/10.1093/logcom/exm037
https://doi.org/10.1093/logcom/exm037
Autor:
Mariangiola Dezani-Ciancaglini, Steffen van Bakel, Pierre Lescanne, Daniel J. Dougherty, Stéphane Lengrand
Publikováno v:
Information and Computation
Information and Computation, 2004, 189 (1), pp.17-42
Information and Computation, Elsevier, 2004, 189 (1), pp.17-42
Information and Computation, 2004, 189 (1), pp.17-42
Information and Computation, Elsevier, 2004, 189 (1), pp.17-42
We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are strongly normalizing. This system extends previous work o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a22a9f974930cb021b275b17695da142
https://doi.org/10.1016/j.ic.2003.09.004
https://doi.org/10.1016/j.ic.2003.09.004
Autor:
Stéphane Lengrand
Publikováno v:
Post-proceedings of the 3rd Workshop on Reduction Strategies in Rewriting and Programming (WRS'03)
Nov 2003, pp.714-730
Nov 2003, pp.714-730
We present a typed calculus λξ isomorphic to the implicational fragment of the classical sequent calculus LK. Reductions in LK eliminate the cut-rule by local rewriting steps, which correspond to the evaluation of explicit substitutions in the calc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4d733108be1368b4a91901584c37775a
https://doi.org/10.1016/s1571-0661(05)82619-2
https://doi.org/10.1016/s1571-0661(05)82619-2
Autor:
Stéphane Lengrand, Alexis Bernadet
We present a typing system with non-idempotent intersection types, typing a term syntax covering three different calculi: the pure {\lambda}-calculus, the calculus with explicit substitutions {\lambda}S, and the calculus with explicit substitutions,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::55f17258945ecbceac7c3085e0e06f7a
http://arxiv.org/abs/1310.1622
http://arxiv.org/abs/1310.1622
Autor:
Murdoch J. Gabbay, Stéphane Lengrand
Publikováno v:
Information and Computation.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::71be9ebd245482be5d76b8155f1f2217
https://doi.org/10.1016/j.ic.2012.01.001
https://doi.org/10.1016/j.ic.2012.01.001
Autor:
Alexis Bernadet, Stéphane Lengrand
Publikováno v:
Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'11)
Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'11), Sep 2011, Saarbruecken, Germany. pp.88-107, ⟨10.1007/978-3-642-19805-2_7⟩
Foundations of Software Science and Computational Structures ISBN: 9783642198045
FoSSaCS
Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'11), Sep 2011, Saarbruecken, Germany. pp.88-107, ⟨10.1007/978-3-642-19805-2_7⟩
Foundations of Software Science and Computational Structures ISBN: 9783642198045
FoSSaCS
International audience; We present a typing system for the λ-calculus, with non-idempotent intersection types. As it is the case in (some) systems with idempotent intersections, a λ-term is typable if and only if it is strongly normalising. Non-ide
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f14be37fa080edaecc027ab0c4fc6f10
https://hal.archives-ouvertes.fr/hal-01110489
https://hal.archives-ouvertes.fr/hal-01110489
Publikováno v:
Logical Methods in Computer Science
Logical Methods in Computer Science, 2011, 7 (1), pp.33. ⟨10.2168/LMCS-7(1:6)2011⟩
Lengrand, S, Dyckhoff, R & McKinna, J 2011, ' A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems ', Logical Methods in Computer Science, vol. 7, no. 1, 6 . https://doi.org/10.2168/LMCS-7(1:6)2011
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2011, 7 (1), pp.33. ⟨10.2168/LMCS-7(1:6)2011⟩
Logical Methods in Computer Science, 2011, 7 (1), pp.33. ⟨10.2168/LMCS-7(1:6)2011⟩
Lengrand, S, Dyckhoff, R & McKinna, J 2011, ' A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems ', Logical Methods in Computer Science, vol. 7, no. 1, 6 . https://doi.org/10.2168/LMCS-7(1:6)2011
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2011, 7 (1), pp.33. ⟨10.2168/LMCS-7(1:6)2011⟩
Basic proof-search tactics in logic and type theory can be seen as the root-first applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper addresses the issues of defi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a667d0b95f9c108884c8ba84182ca6f5
https://hal.science/hal-01110478/file/TTSC09.pdf
https://hal.science/hal-01110478/file/TTSC09.pdf
Autor:
Kentaro Kikuchi, Stéphane Lengrand
Publikováno v:
Foundations of Software Science and Computational Structures ISBN: 9783540784975
FoSSaCS
FoSSaCS
This paper is concerned with strong normalisation of cut-elimination for a standard intuitionistic sequent calculus. The cut-elimination procedure is based on a rewrite system for proof-terms with cut-permutation rules allowing the simulation of β-r
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a5fcae35a833722009c1172ac68debc6
https://doi.org/10.1007/978-3-540-78499-9_27
https://doi.org/10.1007/978-3-540-78499-9_27