60 citations
- Université Paris-SaclayFR43 papers
- Centre National de la Recherche ScientifiqueFR36 papers
- CentraleSupélecFR17 papers
- Institut national de recherche en sciences et technologies du numériqueFR14 papers
- École Normale Supérieure - PSLFR11 papers
- École Normale Supérieure Paris-SaclayFR8 papers
- Laboratoire de Biologie et Pharmacologie AppliquéeFR8 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR8 papers
- Centre Inria de SaclayFR6 papers
- Institut Universitaire de FranceFR6 papers
- Université de LorraineFR6 papers
- Aix-Marseille UniversitéFR5 papers
6 papers · 2 filters
A strong call-by-need calculus
Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
We present a call-by-need -calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed…
A modular construction of type theories
Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger +2
The lambda-Pi-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several…
Proceedings 17th International Conference on Quantum Physics and Logic
Benoît Valiron, Shane Mansfield, Pablo Arrighi +1
This volume contains the proceedings of the 17th International Conference on Quantum Physics and Logic (QPL 2020), which was held June 2-6, 2020. Quantum Physics and Logic is an an…
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving
Chantal Keller, Mathias Fleury
This volume of EPTCS contains the proceedings of the Seventh Workshop on Proof Exchange for Theorem Proving (PxTP 2021), held on 11 July 2021 as part of the CADE-28 online conferen…
Bounded Reachability Problems are Decidable in FIFO Machines
Benedikt Bollig, Alain Finkel, Amrita Suresh
The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for th…
Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
Bartosz Bednarczyk, Stéphane Demri
Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) adm…