77 citations
- Université Paris-Est CréteilFR14 papers
- Centre National de la Recherche ScientifiqueFR7 papers
- Laboratoire d'Informatique Algorithmique: Fondements et ApplicationsFR5 papers
- Paris-Est SupFR5 papers
- Institute of Mathematics and Computer ScienceMD3 papers
- Université Paris DiderotFR3 papers
- Åbo Akademi UniversityFI2 papers
- Institut de Mécanique et d'Ingénierie de BordeauxFR2 papers
- Institut national de recherche en sciences et technologies du numériqueFR2 papers
- Laboratoire d'Informatique de Paris-NordFR2 papers
- Laboratoire d'Informatique Gaspard-MongeFR2 papers
- Laboratoire Spécification et VérificationFR2 papers
4 papers · 2 filters
Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control
Tristan Crolard, Emmanuel Polonowski
We derive a Hoare-Floyd logic for non-local jumps and mutable higher-order procedural variables from a formulæ-as-types notion of control for classical logic. The main contribution…
A program logic for higher-order procedural variables and non-local jumps
Tristan Crolard, Emmanuel Polonowski
Relying on the formulae-as-types paradigm for classical logic, we define a program logic for an imperative language with higher-order procedural variables and non-local jumps. Then…
Generic Environments in Coq
Emmanuel Polonowski
We introduce a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for…
Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
Catalin Dima, Ferucio Laurentiu Tiplea
We propose a formal proof of the undecidability of the model checking problem for alternating- time temporal logic under imperfect information and perfect recall semantics. This pr…