Papers
The following papers present results from the PiCoq project.
- Daniel Hirschkoff and Jean-Marie Madiot and Xian
Xu. A behavioural theory for a pi-calculus with
preorders. In Proceeding of FSEN 2015, LNCS, to
appear.
- Martín Escarrá, Maksimović Petar, Alan Schmitt. HOCore in
Coq. In Actes des Vingt-sixièmes Journées Francophones des
Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol,
France. [hal]
- Paul Brunet, Damien Pous. Decidability of Identity-free
Relational Kleene Lattices. In Actes des Vingt-sixièmes Journées
Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le
Val d'Ajol,
France. [hal]
- Damien Pous. Symbolic algorithms for language equivalence and
kleene algebra with tests. In Proceedings of POPL. ACM,
2015. [hal]
- Jean-Bernard Stefani. Components as Location Graphs. In 11th
International Symposium on Formal Aspects of Component
Software, volume 8997 of Lecture Notes in Computer Science,
Bertinoro, Italy,
2014. [hal]
- Tom Hirschowitz. Full abstraction for fair testing in CCS
(expanded version). In Logical Methods in Computer Science,
10(4),
2014. [hal]
- Jean-Marie Madiot, Damien Pous, Davide Sangiorgi. Bisimulations
Up-to: Beyond First-Order Transition Systems. In Proceedings
of CONCUR 2014, 93-108, LNCS, Springer
Verlag. [pdf]
- Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan
Rot. Coinduction up-to in a fibrational setting. In Proceedings
of CSL-LICS. ACM,
2014. [hal]
- Paul Brunet and Damien Pous. Kleene algebra with
converse. In Proceedings of RAMiCS, volume 8428 of LNCS,
pages 101-118. Springer,
2014. [hal]
- Damien Pous and Alan Schmitt. De la KAM avec un processus
d'ordre supérieur. In Actes des 25èmes Journées Francophones des
Langages Applicatifs. INRIA,
2014. [hal]
- Filippo Bonchi, Georgiana Caltais, Damien Pous, and Alexandra
Silva. Brzozowski's and Up-To Algorithms for Must Testing.
In Proceedings of APLAS 2013, LNCS 8301, December 2013.
[pdf]
- Damien Pous. Kleene Algebra with Tests and Coq Tools for while
Programs. In Proceedings of ITP 2013, pages 180-196.
[hal].
- Tom Hirschowitz. Cartesian closed 2-categories and permutation
equivalence in higher-order rewriting. In Logical Methods in
Computer Science, 9(3), 2013.
[hal]
- Damien Pous. Coalgebraic Up-to Techniques. In Proceedings of
CALCO'13, pages 34-35.
[pdf]
- Tom Hirschowitz. Full abstraction for fair testing in CCS.
In Proceedings of CALCO'13.
[hal]
- Daniel Hirschkoff, Jean-Marie Madiot, Davide Sangiorgi.
Name-passing calculi: from fusions to preorders and types.
In Proceedings of LICS'13.
[pdf,
hal]
- Ivan Lanese, Michal Lienhardt, Claudio Antares Mezzina, Alan
Schmitt, and Jean-Bernard Stefani. Concurrent Flexible Reversibility.
In Proceedings of ESOP'13.
[pdf,hal]
- Filippo Bonchi and Damien Pous. Checking nfa equivalence with
bisimulations up to congruence. In Proceedings of
POPL'13. [pdf,
hal]
- Damien Pous. Untyping Typed Algebras and Colouring Cyclic Linear
Logic. In Logical Methods in Computer Science, 2012. [pdf]
- Thomas Braibant and Damien Pous. Deciding Kleene Algebras in Coq. In Logical Methods in Computer Science 8(1): (2012).
- Daniel Hirschkoff, Jean-Marie Madiot, and Davide
Sangiorgi. Duality and i/o-types in the
p-calculus. In Proceedings of CONCUR'12, LNCS. Springer
Verlag, 2012.
- Tom Hirschowitz and Damien Pous. Innocent strategies as presheaves
and interactive equivalences for CCS. Scientific Annals of
Computer Science, volume XXII (1), pages 147-199. University of
Iaşi, 2012.
[hal]
- Simon Boulier and Alan Schmitt. Formalisation de HOCore en Coq.
In Actes des 23èmes Journées Francophones des Langages
Applicatifs, January 2012.
[pdf]
- Thomas Braibant. Coquet: a Coq library for verifying hardware. In Proceedings of 1st CPP, volume 7086 of Lecture Notes in Computer Science. Springer, 2011.[pdf]
- Thomas Braibant and Damien Pous. Tactics for reasoning modulo AC in Coq. In Proceedings of 1st CPP, volume 7086 of Lecture Notes in Computer Science, pages 167–182. Springer, 2011.[pdf]
- Ivan Lanese, Claudio Antares Mezzina, Alan Schmitt, and
Jean-Bernard Stefani. Controlling reversibility in higher-order pi. In
Proceedings of the 22nd International Conference on Concurrency Theory
(CONCUR 2011), volume 6901 of Lecture Notes in Computer Science, pages
297–311, Aachen, Germany, September 2011. Springer.[pdf]
- Ioana Cristescu and Daniel Hirschkoff. Termination in a pi-calculus with subtyping. In Bas Luttik and Frank Valencia, editors, EXPRESS, volume 64 of EPTCS, page 44, 2011. [pdf]
- Tom Hirschowitz and Damien Pous. Innocent strategies as presheaves and interactive equivalences for ccs. In ICE'11, volume 59 of EPTCS, pages 2–24, 2011.[pdf]
- Cinzia Di Giusto and Jean-Bernard Stefani. Revisiting glues for component-based systems. In 13th International Conference on Coordination Models and Languages (COORDINATION), volume 6721 of Lecture Notes in Computer Science. Springer, 2011. [pdf]
Deliverables
2014:
D123, D4, D5.
2013:
D123, D4, D5.
2012:
D123, D4, D5.
2011:
D123, D4, D5.
