490 citations
Counting papers with at most 25 authors, so collaboration author lists do not stand in for the people here.
- Institut national de recherche en sciences et technologies du numériqueFR110 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR87 papers
- Centre National de la Recherche ScientifiqueFR55 papers
- Université de LorraineFR43 papers
- Institut Élie Cartan de LorraineFR35 papers
- Université de StrasbourgFR10 papers
- École PolytechniqueFR9 papers
- Laboratoire des Sciences de l'Ingénieur, de l'Informatique et de l'ImagerieFR9 papers
- University of LuxembourgLU8 papers
- Institut de Recherche Mathématique AvancéeFR7 papers
- Centre de Mathématiques Appliquées de l'École polytechniqueFR5 papers
- Computer Algorithms for MedicineAT5 papers
13 papers · 1 filter
Extending Nunchaku to Dependent Type Theory
Simon Cruanes, Jasmin Christian Blanchette
Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitp…
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Damien Doligez, Jael Kriener, Leslie Lamport +2
We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.
A correspondence between rooted planar maps and normal planar lambda terms
Noam Zeilberger, Alain Giorgetti
A rooted planar map is a connected graph embedded in the 2-sphere, with one edge marked and assigned an orientation. A term of the pure lambda calculus is said to be linear if ever…
A Vernacular for Coherent Logic
Sana Stojanovic, Julien Narboux, Marc Bezem +1
We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rule…
Unification modulo a 2-sorted Equational theory for Cipher-Decipher Block Chaining
Siva Anantharaman, Christopher Bouchard, Paliath Narendran +1
We investigate unification problems related to the Cipher Block Chaining (CBC) mode of encryption. We first model chaining in terms of a simple, convergent, rewrite system over a s…
Normalization and sub-formula property for Lambek with product and PCMLL -- Partially Commutative Multiplicative Linear Logic
Maxime Amblard, Christian Retoré
This paper establishes the normalisation of natural deduction or lambda calculus formulation of Intuitionistic Non Commutative Logic --- which involves both commutative and non com…
Generalization Strategies for the Verification of Infinite State Systems
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti +1
We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic prog…
Verifying Safety Properties With the TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport +1
TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond element…
A Type System for Tom
Claude Kirchner, Pierre-Etienne Moreau, Cláudia Tavares
Extending a given language with new dedicated features is a general and quite used approach to make the programming language more adapted to problems. Being closer to the applicati…
Intensional properties of polygraphs
Guillaume Bonfante, Yves Guiraud
We present polygraphic programs, a subclass of Albert Burroni's polygraphs, as a computational model, showing how these objects can be seen as first-order functional programs. We p…
On the implementation of construction functions for non-free concrete data types
Frédéric Blanqui, Thérèse Hardin, Pierre Weis
Many algorithms use concrete data types with some additional invariants. The set of values satisfying the invariants is often a set of representatives for the equivalence classes o…
Polygraphic programs and polynomial-time functions
Guillaume Bonfante, Yves Guiraud
We study the computational model of polygraphs. For that, we consider polygraphic programs, a subclass of these objects, as a formal description of first-order functional programs.…
Inductive types in the Calculus of Algebraic Constructions
Frédéric Blanqui
In a previous work, we proved that almost all of the Calculus of Inductive Constructions (CIC), which is the basis of the proof assistant Coq, can be seen as a Calculus of Algebrai…