242 citations
- Institut national de recherche en sciences et technologies du numériqueFR106 papers
- Laboratoire de Recherche en InformatiqueFR19 papers
- École PolytechniqueFR10 papers
- Université Paris-SudFR10 papers
- Commissariat à l'Énergie Atomique et aux Énergies AlternativesFR9 papers
- Centre National de la Recherche ScientifiqueFR8 papers
- Laboratoire d'Informatique de l'École PolytechniqueFR8 papers
- InsermFR6 papers
- Laboratoire de Mathématiques d'OrsayFR5 papers
- CEA Paris-SaclayFR4 papers
- Laboratoire de Mathématiques Blaise PascalFR4 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR4 papers
4 papers · 2 filters
Partition Refinement for Bisimilarity in CCP
Andrés Aristizábal, Filippo Bonchi, Luis Pino +1
Saraswat's concurrent constraint programming (ccp) is a mature formalism for modeling processes (or programs) that interact by telling and asking constraints in a global medium, ca…
The Refined Calculus of Inductive Construction: Parametricity and Abstraction
Chantal Keller, Marc Lasson
We present a refinement of the Calculus of Inductive Constructions in which one can easily define a notion of relational parametricity. It provides a new way to automate proofs in…
Two simulations about DPLL(T)
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
In this paper we relate different formulations of the DPLL(T) procedure. The first formulation is based on a system of rewrite rules, which we denote DPLL(T). The second formulatio…
A sequent calculus with procedure calls
Mahfuza Farooque, Stéphane Lengrand
In this paper, we extend the sequent calculus LKF into a calculus LK(T), allowing calls to a decision procedure. We prove cut-elimination of LK(T).