Zobrazeno 1 - 10
of 70
pro vyhledávání: '"Christophe Raffalli"'
Autor:
Rodolphe Lepigre, Christophe Raffalli
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 42-56 (2018)
The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a do
Externí odkaz:
https://doaj.org/article/65ae903d330f4cb0baa8eb25eaf94ed0
Autor:
Christophe Raffalli, Rodolphe Lepigre
Publikováno v:
ACM Transactions on Programming Languages and Systems. 41:1-58
We present a new, syntax-directed framework for Curry-style type systems with subtyping. It supports a rich set of features, and allows for a reasonably simple theory and implementation. The system we consider has sum and product types, universal and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1ddab98b91493fed7c78d906afbbd059
https://doi.org/10.1145/3285955
https://doi.org/10.1145/3285955
Autor:
René David, Katarzyna Grygiel, Jakub Kozik, Christophe Raffalli, Guillaume Theyssier, Marek Zaionc
Publikováno v:
Logical Methods in Computer Science, Vol Volume 9, Issue 1 (2013)
We present quantitative analysis of various (syntactic and behavioral) properties of random \lambda-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random
Externí odkaz:
https://doaj.org/article/b5a82658aead44a5acc075a46de8a113
Autor:
Christophe Raffalli, Rodolphe Lepigre
Publikováno v:
Electronic Proceedings in Theoretical Computer Science
Electronic Proceedings in Theoretical Computer Science, EPTCS, 2018, 274, pp.42-56. ⟨10.4204/EPTCS.274.4⟩
Electronic Proceedings in Theoretical Computer Science, 2018, 274, pp.42-56. ⟨10.4204/EPTCS.274.4⟩
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 42-56 (2018)
LFMTP@FSCD
Electronic Proceedings in Theoretical Computer Science, EPTCS, 2018, 274, pp.42-56. ⟨10.4204/EPTCS.274.4⟩
Electronic Proceedings in Theoretical Computer Science, 2018, 274, pp.42-56. ⟨10.4204/EPTCS.274.4⟩
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 42-56 (2018)
LFMTP@FSCD
The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a do
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::af2742b51dd3b5b491081c545006cb41
https://hal.inria.fr/hal-01972050
https://hal.inria.fr/hal-01972050
Autor:
Christophe Raffalli
Publikováno v:
Annals of Pure and Applied Logic. 122:107-130
We introduce a new type system called “System ST” (ST stands for subtyping), based on subtyping, and prove the basic property of the system. We show the extraordinary expressive power of the system which leads us to think that it could be a good
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c8d5ddf3710351dfe788deef7cf3d01c
https://doi.org/10.1016/s0168-0072(03)00002-2
https://doi.org/10.1016/s0168-0072(03)00002-2
Autor:
Christophe Raffalli
Publikováno v:
Theoretical Computer Science. 254:259-271
We formalize, in the AF 2 -type system, a completeness and correctness theorem for a modified Kripke semantics for minimal logic. We show that any program extracted from a proof of the completeness theorem translates higher-order encoding of a λ -te
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8db33076916e31a4bf169f243a7f5ef8
https://doi.org/10.1016/s0304-3975(99)00141-3
https://doi.org/10.1016/s0304-3975(99)00141-3
Autor:
Christophe Raffalli
Publikováno v:
Annals of Pure and Applied Logic. 91:17-31
Storage operators are λ-terms which simulate call-by-value in call-by-name for a given set of terms. Krivine's storage operator theorem shows that any term of type ¬D → ¬D∗, where D∗ is the Godel translation of D, is a storage operator for t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a99bb5a154f619154a67f93d6938f7f1
https://doi.org/10.1016/s0168-0072(97)00041-9
https://doi.org/10.1016/s0168-0072(97)00041-9
Autor:
Christophe Raffalli, Muhammad Humayoun
Publikováno v:
FIT
MathAbs (Mathematical Abstract language) is a system independent formal language for mathematical texts that can preserve its structure including the line of reasoning, proof steps and logical structure. By system independent, we mean that its formal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d260d1f0a8a02139185f6277d134ea04
https://doi.org/10.1145/1943628.1943665
https://doi.org/10.1145/1943628.1943665
Autor:
Christophe Raffalli, Katarzyna Grygiel, Henk Barendregt, René David, Jakub Kozik, Guillaume Theyssier, Marek Zaionc
We present quantitative analysis of various (syntactic and behavioral) properties of random \lambda-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::30ed009429218ddb2d9945238bd225f2
http://arxiv.org/abs/0903.5505
http://arxiv.org/abs/0903.5505
Autor:
Christophe Raffalli
Publikováno v:
Computer Science Logic ISBN: 3540582770
CSL
CSL
This work presents an extension of system AF2 to allow the use of infinite data types. We extend the logic with inductive and coinductive types, and show that the “programming method” is still correct. We prove propositions about the normalizatio
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f1f1634481d7b386acc866075bc3f6fb
https://doi.org/10.1007/bfb0049337
https://doi.org/10.1007/bfb0049337