Zobrazeno 1 - 7
of 7
pro vyhledávání: '"Rodolphe Lepigre"'
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:
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
Publikováno v:
Proceedings of the ACM on Programming Languages
49th ACM SIGPLAN Symposium on Principles of Programming Languages
PACM PL (POPL)
Proceedings of the ACM on Programming Languages, 6, 1-32
Proceedings of the ACM on Programming Languages, 6, POPL, pp. 1-32
49th ACM SIGPLAN Symposium on Principles of Programming Languages
PACM PL (POPL)
Proceedings of the ACM on Programming Languages, 6, 1-32
Proceedings of the ACM on Programming Languages, 6, POPL, pp. 1-32
Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level ( e.g. , bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they are performed
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a24092bc6a216320ea29e35744ab0ad9
https://hdl.handle.net/21.11116/0000-0009-C4F0-A21.11116/0000-0009-C4F2-8
https://hdl.handle.net/21.11116/0000-0009-C4F0-A21.11116/0000-0009-C4F2-8
Publikováno v:
Proceedings of the ACM on Programming Languages
ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
Low-level systems code often needs to interact with data, such as page table entries or network packet headers, in which multiple pieces of information are packaged together as bitfield components of a single machine integer and accessed via bitfield
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::104ab9eb8dc7cefa9f2c60f7e3249374
https://hdl.handle.net/21.11116/0000-000B-5E70-E21.11116/0000-000B-5E72-C
https://hdl.handle.net/21.11116/0000-000B-5E70-E21.11116/0000-000B-5E72-C
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:
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:
Rodolphe Lepigre
Publikováno v:
Programming Languages and Systems ISBN: 9783662494974
ESOP
ESOP
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 for
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7fb1224f1f01806caf350b542fdb58d5
https://doi.org/10.1007/978-3-662-49498-1_19
https://doi.org/10.1007/978-3-662-49498-1_19
Autor:
Gaurav Parthasarathy, Rodolphe Lepigre, Amin Timany, Ralf Jung, Marianna Rapoport, Derek Dreyer, Bart Jacobs
Publikováno v:
Proceedings of the ACM on Programming Languages, 4 (POPL)
Jung, R, Lepigre, R, Parthasarathy, G, Rapoport, M, Timany, A, Dreyer, D & Jacobs, B 2020, ' The future is ours: prophecy variables in separation logic ', PACMPL, bind 4, nr. POPL, s. 45:1-45:32 . https://doi.org/10.1145/3371113
Proceedings of the ACM on Programming Languages
Jung, R, Lepigre, R, Parthasarathy, G, Rapoport, M, Timany, A, Dreyer, D & Jacobs, B 2020, ' The future is ours: prophecy variables in separation logic ', PACMPL, bind 4, nr. POPL, s. 45:1-45:32 . https://doi.org/10.1145/3371113
Proceedings of the ACM on Programming Languages
Early in the development of Hoare logic, Owicki and Gries introduced auxiliary variables as a way of encoding information about the history of a program’s execution that is useful for verifying its correctness. Over a decade later, Abadi and Lampor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7c236b5aabc231aaa0752bdc80fdd99d