77 citations
- Institute of Mathematics and Computer ScienceMD2 papers
- Åbo Akademi UniversityFI1 paper
- Département d'InformatiqueFR1 paper
- Informatique, BioInformatique, Systèmes ComplexesFR1 paper
- Laboratoire d'Informatique Algorithmique: Fondements et ApplicationsFR1 paper
- Laboratoire d'informatique de Nantes AtlantiqueFR1 paper
- Nantes UniversitéFR1 paper
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2011★ 77 cited
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…
cs.LO2009
A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables
Tristan Crolard, Emmanuel Polonowski
We formally specified the type system and operational semantics of LOOPw with Ott and Isabelle/HOL proof assistant. Moreover, both the type system and the semantics of LOOPw have b…
cs.LO2009
Deriving SN from PSN: a general proof technique
Emmanuel Polonowski
In the framework of explicit substitutions there is two termination properties: preservation of strong normalization (PSN), and strong normalization (SN). Since there are not easil…