11 citations
- Institut national de recherche en sciences et technologies du numériqueFR2 papers
- Laboratory Preuves, Programmes et SystèmesFR2 papers
- École Normale Supérieure - PSLFR1 paper
- ElSohly Laboratories (United States)US1 paper
- Laboratoire d'Informatique, de Robotique et de Microélectronique de MontpellierFR1 paper
- Laboratoire d'Informatique et d'Automatique pour les SystèmesFR1 paper
- Pressure Profile Systems (United States)US1 paper
6 papers
A Substructural Epistemic Resource Logic: Theory and Modelling Applications
Didier Galmiche, Pierre Kimmel, David Pym
We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents' local resources. The new modalities can be seen as ge…
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
Théo Zimmermann, Hugo Herbelin
In mathematics, it is common practice to have several constructions for the same objects. Mathematicians will identify them modulo isomorphism and will not worry later on which con…
Operads, clones, and distributive laws
Pierre-Louis Curien
We show how non-symmetric operads (or multicategories), symmetric operads, and clones, arise from three suitable monads on Cat, each extending to a (pseudo-)monad on the bicategory…
Verification of Timed Automata Using Rewrite Rules and Strategies
Emmanuel Beffara, Olivier Bournez, Hassen Kacem +1
ELAN is a powerful language and environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies. Timed automata is a clas…
Formal proof for delayed finite field arithmetic using floating point operators
Sylvie Boldo, Marc Daumas, Pascal Giorgi
Formal proof checkers such as Coq are capable of validating proofs of correction of algorithms for finite field arithmetics but they require extensive training from potential users…
Termination of rewriting strategies: a generic approach
Isabelle Gnaedig, Helene Kirchner
We propose a generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modele…