Zobrazeno 1 - 10
of 20
pro vyhledávání: '"Lepigre, Rodolphe"'
Autor:
Lepigre, Rodolphe
Publikováno v:
23rd International Conference on Types for Proofs and Programs (TYPES 2017), Jul 2017, Budapest, Hungary. pp.27, 2018
We present the PML 2 language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of
Externí odkaz:
http://arxiv.org/abs/1901.03208
Autor:
Lepigre, Rodolphe
Au cours des dernières années, les assistants de preuves on fait des progrès considérables et ont atteint un grand niveau de maturité. Ils ont permit la certification de programmes complexes tels que des compilateurs et même des systèmes d'exp
Externí odkaz:
http://www.theses.fr/2017GREAM034/document
In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single field) can sometimes be `unboxed'. This means that their memory representation is the same as their single argument (omitting the varian
Externí odkaz:
http://arxiv.org/abs/1811.02300
Publikováno v:
EPTCS 274, 2018, pp. 42-56
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:
http://arxiv.org/abs/1807.01872
We present a rich type system with subtyping for an extension of System F. Our type constructors include sum and product types, universal and existential quantifiers, inductive and coinductive types. The latter two size annotations allowing the prese
Externí odkaz:
http://arxiv.org/abs/1604.01990
Autor:
Lepigre, Rodolphe
We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used fo
Externí odkaz:
http://arxiv.org/abs/1603.07484
Publikováno v:
ACM Transactions on Programming Languages & Systems. Mar2019, Vol. 41 Issue 1, p1-58. 58p.
Autor:
Lepigre, Rodolphe
Publikováno v:
Computer Science [cs]. Grenoble 1 UGA-Université Grenoble Alpes, 2017. English
In recent years, proof assistant have reached an impressive level of maturity. They have led to the certification of complex programs such as compilers and operating systems. Yet, using a proof assistant requires highly specialised skills and it rema
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::2d97d9f59b483f814a15d9bc3b321964
https://hal.inria.fr/tel-01590363
https://hal.inria.fr/tel-01590363
Autor:
Lepigre, Rodolphe
We present the PML_2 language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e82277e9847772124c566fd1739bcf03
We present a rich type system with subtyping for an extension of System F. Our type constructors include sum and product types, universal and existential quantifiers, inductive and coinductive types. The latter two size annotations allowing the prese
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e47862deef39952b8bf961fd211ec02b
https://hal.archives-ouvertes.fr/hal-01289760
https://hal.archives-ouvertes.fr/hal-01289760