Výsledky vyhledávání - "Kenji Maillard"

SSProve: A foundational framework for modular cryptographic proofs in Coq

Autor: Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Cătălin Hrițcu, Kenji Maillard, Bas Spitters

Publikováno v: ACM Transactions on Programming Languages and Systems.

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously n

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::527ef3480187e0fa65e80de3b22ec333
https://doi.org/10.1145/3594735

Zobrazit plný text záznamu

A Reasonably Gradual Type Theory

Autor: Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, In press
HAL

Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently, GCIC has been proposed as a parametrized gradual type theory that ad

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2f08ecfbb2b5d492fe2fda1321a62060
http://arxiv.org/abs/2209.00975

Zobrazit plný text záznamu

Gradualizing the Calculus of Inductive Constructions

Autor: Kenji Maillard, Meven Lennon-Bertrand, Éric Tanter, Nicolas Tabareau

Publikováno v: ACM Transactions on Programming Languages and Systems (TOPLAS)
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2022, ⟨10.1145/3495528⟩
ACM Transactions on Programming Languages and Systems (TOPLAS), 2022, ⟨10.1145/3495528⟩

We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial tradeoff between graduality and the key properties of normalization

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bb63199d40af44d2995c6dc35639d6dc
https://hal.archives-ouvertes.fr/hal-02896776v4/document

Zobrazit plný text záznamu

Principles of program verification for arbitrary monadic effects

Autor: Kenji Maillard

Publikováno v: Programming Languages [cs.PL]. Université Paris sciences et lettres, 2019. English. ⟨NNT : 2019PSLEE081⟩
Computer Science [cs]. ENS Paris-Ecole Normale Supérieure de Paris, 2019. English
HAL

Computational monads are a convenient algebraic gadget to uniformly represent side-effects in programming languages, such as mutable state, divergence, exceptions, or non-determinism. Various frameworks for specifying programs and proving that they m

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::54dacb3e3da567e5028279df624333bd
https://tel.archives-ouvertes.fr/tel-03441023v2/document

Zobrazit plný text záznamu

A preview of a tutorial on L (polarized μμ-tilde)

Autor: Kenji Maillard, Étienne Miquey, Xavier Montillet, Guillaume Munch-Maccagnoni, Gabriel Scherer

Publikováno v: HOPE 2018-7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects
HOPE 2018-7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, Sep 2018, St. Louis, United States
HAL

International audience; We are working on a new tutorial presentation of L, the polarized version of Curien-Herbelin’s μμ̃ -calculus. The calculus μμ̃ was introduced in Curien and Herbelin [2000] as a good term calculus for classical logic, w

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::335d382098e1f2c032a4eb353519e0ff
https://inria.hal.science/hal-01992294

Zobrazit plný text záznamu

Recalling a witness: foundations and applications of monotonic state

Autor: Nikhil Swamy, Aseem Rastogi, Cătălin Hriţcu, Danel Ahman, Cédric Fournet, Kenji Maillard

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), ⟨10.1145/3158153⟩
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), ⟨10.1145/3158153⟩

We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the current state, provided (1) state evolves according to a given preorde

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::96c4ad18cd51e1e9c86681b3b7f880c4

Zobrazit plný text záznamu

A Fibrational Account of Local States

Autor: Paul-André Melliès, Kenji Maillard

Publikováno v: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2015, Kyoto, France. pp.402-413, ⟨10.1109/LICS.2015.45⟩
LICS

International audience; One main challenge of the theory of computational effects is to understand how to combine various notions of effects in a meaningful way. Here, we study the particular case of the local state monad, which we would like to expr

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::87484a60bdd7d806bea0fbade02495ba
https://hal.inria.fr/hal-03066087/document

Zobrazit plný text záznamu

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations

Autor: Jonathan Protzenko, Cătălin Hriţcu, Niklas Grimm, Tahina Ramananandro, Kenji Maillard, Aseem Rastogi, Cédric Fournet, Nikhil Swamy, Santiago Zanella-Béguelin, Matteo Maffei

Publikováno v: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs -CPP 2018
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs-CPP 2018
CPP

Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f81fa6607928a4368b134ec59e892f25

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání