Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

Autor: Paulo Emílio de Vilhena, François Pottier

Publikováno v: Logical Methods in Computer Science, Vol Volume 19, Issue 4 (2023)

We apply program verification technology to the problem of specifying and verifying automatic differentiation (AD) algorithms. We focus on define-by-run, a style of AD where the program that must be differentiated is executed and monitored by the aut

Externí odkaz: https://doaj.org/article/c3eb8936345649fda3bf96782f94e5cb

A Type System for Effect Handlers and Dynamic Labels

Autor: Paulo Emílio de Vilhena, François Pottier

Publikováno v: Programming Languages and Systems ISBN: 9783031300431

We consider a simple yet expressive $$\lambda $$ λ -calculus equipped with references, effect handlers, and dynamic allocation of effect labels, and whose operational semantics does not involve coercions or rely on type information. We equip this la

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::2a19cc61d7dc9f7508574ba63a9be869
https://doi.org/10.1007/978-3-031-30044-8_9

Specification and Verification of a Transient Stack

Autor: Alexandre Moine, Arthur Charguéraud, François Pottier

Publikováno v: CPP 2022-11th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP 2022-11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. ⟨10.1145/3497775.3503677⟩

International audience; A transient data structure is a package of an ephemeral data structure, a persistent data structure, and fast conversions between them. We describe the specification and proof of a transient stack and its iterators. This data

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4ec834bd1adabfaa65bce2b975b82fb0
https://hal.inria.fr/hal-03472028

Faster reachability analysis for LR(1) parsers

Autor: François Pottier, Frédéric Bour

Publikováno v: SLE 2021-ACM SIGPLAN International Conference on Software Language Engineering
SLE 2021-ACM SIGPLAN International Conference on Software Language Engineering, Oct 2021, Chicago, United States. ⟨10.1145/3486608.3486903⟩
SLE

International audience; We present a novel algorithm for reachability in an LR(1) automaton. For each transition in the automaton, the problem is to determine under what conditions this transition can be taken, that is, which (minimal) input fragment

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::07dd0b231e5121cb39323506b60ab667
https://hal.inria.fr/hal-03478172

A Simple, Possibly Correct LR Parser for C11

Autor: Jacques-Henri Jourdan, François Pottier

Publikováno v: ACM Transactions on Programming Languages and Systems (TOPLAS)
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2017, 39 (4), pp.1-36. ⟨10.1145/3064848⟩
ACM Transactions on Programming Languages and Systems (TOPLAS), 2017, 39 (4), pp.1-36. ⟨10.1145/3064848⟩

International audience; The syntax of the C programming language is described in the C11 standard by an ambiguous context-free grammar, accompanied with English prose that describes the concept of " scope " and indicates how certain ambiguous code fr

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::33a46063777587db07c9fd0a434b2a26
https://doi.org/10.1145/3064848