29.3k citations
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR55 papers
- Centre National de la Recherche ScientifiqueFR24 papers
- Institut de Recherche en Informatique et Systèmes AléatoiresFR11 papers
- Université Paris CitéFR9 papers
- Laboratoire de l'Informatique du ParallélismeFR8 papers
- Université de LorraineFR8 papers
- Institut Élie Cartan de LorraineFR7 papers
- Université Paris-SudFR7 papers
- Computer Algorithms for MedicineAT6 papers
- Laboratoire d'Informatique Algorithmique: Fondements et ApplicationsFR6 papers
- Laboratoire d'Informatique de GrenobleFR6 papers
- Sorbonne UniversitéFR6 papers
10 papers · 1 filter
Encapsulation and Dynamic Modularity in the Pi-Calculus
Daniel Hirschkoff, Aurélien Pardon, Tom Hirschowitz +2
We describe a process calculus featuring high level constructs for component-oriented programming in a distributed setting. We propose an extension of the higher-order pi-calculus…
Mechanized semantics for the Clight subset of the C language
Sandrine Blazy, Xavier Leroy
This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, "struct" and "union" types, C loops and structured…
Coinductive big-step operational semantics
Xavier Leroy, Hervé Grall
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to de…
Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems - Report on the Workshop ICOOOLPS'2007 at ECOOP'07
Olivier Zendra, Eric Jul, Roland Ducournau +5
ICOOOLPS'2007 was the second edition of the ECOOP-ICOOOLPS workshop. ICOOOLPS intends to bring researchers and practitioners both from academia and industry together, with a spirit…
Separation Logic for Small-step Cminor
Andrew W. Appel, Sandrine Blazy
Cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to Cminor and from Cminor to machine language. We have redesigned Cminor…
Une sémantique observationnelle du modèle des boîtes pour la résolution de programmes logiques (version étendue)
Pierre Deransart, Mireille Ducassé, Gérard Ferrand
This report specifies an observational semantics and gives an original presentation of the Byrd's box model. The approach accounts for the semantics of Prolog tracers independently…