Damien Pous

Christian Doczkal, Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. Journal of Automated Reasoning, Springer Verlag, In press. ⟨hal-02316859v2⟩

Damien Pous, Jurriaan Rot. Companions, Causality and Codensity. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, ⟨10.23638/LMCS-15(3:14)2019⟩. ⟨hal-02330940⟩

Damien Pous, Davide Sangiorgi. Bisimulation and Coinduction Enhancements: A Historical Perspective. Formal Aspects of Computing, Springer Verlag, 2019, 31 (6), pp.733-749. ⟨10.1007/s00165-019-00497-w⟩. ⟨hal-02393949⟩

Paul Brunet, Damien Pous. Petri Automata. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (3), pp.1-50. ⟨10.23638/LMCS-13(3:33)2017⟩. ⟨hal-01934638⟩

Filippo Bonchi, Daniela Petrişan, Damien Pous, Jurriaan Rot. A General Account of Coinduction Up-To. Acta Informatica, Springer Verlag, 2016, ⟨10.1007/s00236-016-0271-4⟩. ⟨hal-01442724⟩

Jurriaan Rot, Filippo Bonchi, Marcello Bonsangue, Damien Pous, Jan Rutten, et al.. Enhanced Coalgebraic Bisimulation. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2015, ⟨10.1017/S0960129515000523⟩. ⟨hal-01288960⟩

Filippo Bonchi, Damien Pous. Hacking nondeterminism with induction and coinduction.. Communications- ACM, Association for Computing Machinery, 2015, 58 (2), pp.87-95. ⟨10.1145/2713167⟩. ⟨hal-01284907⟩

Damien Pous. Untyping Typed Algebras and Colouring Cyclic Linear Logic (expanded). Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, ⟨10.2168/LMCS-8(2:13)2012⟩. ⟨hal-01442739⟩

Tom Hirschowitz, Damien Pous. Innocent strategies as presheaves and interactive equivalences for CCS (expanded version). Scientific Annals of Computer Science, Alexandru Ioan Cuza University Publishing House, 2012, 22 (1), pp.147-199. ⟨10.7561/SACS.2012.1.147⟩. ⟨hal-00555144v3⟩

Damien Pous, Daniel Hirschkoff. A Distribution Law for CCS and a New Congruence Result for the pi-calculus (expanded). Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2008, ⟨10.2168/LMCS-4(2:4)2008⟩. ⟨hal-01442744⟩

Damien Pous. Using Bisimulation Proof Techniques for the Analysis of Distributed Algorithms. Theoretical Computer Science, Elsevier, 2008, 402 (2-3), pp.199-220. ⟨10.1016/j.tcs.2008.04.035⟩. ⟨ensl-00149964v3⟩

Damien Pous. New Up-To Techniques for Weak Bisimulation. Theoretical Computer Science, Elsevier, 2007, 380, pp.164 - 180. ⟨10.1016/j.tcs.2007.02.060⟩. ⟨hal-01442745⟩

Daniel Hirschkoff, Damien Pous, Davide Sangiorgi. An Efficient Abstract Machine for Safe Ambients. Journal of Logic and Algebraic Programming, Elsevier, 2007, ⟨10.1016/j.jlap.2007.02.003⟩. ⟨hal-01442746⟩

Amina Doumane, Damien Pous. Non axiomatisability of positive relation algebras with constants, via graph homomorphisms. CONCUR, 2020, Vienne, Austria. pp.1-23, ⟨10.4230/LIPIcs.CONCUR.2020.49⟩. ⟨hal-02870687v2⟩

Christian Doczkal, Damien Pous. Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq. CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, New Orleans, LA, United States. ⟨10.1145/3372885.3373831⟩. ⟨hal-02333553v3⟩

Denis Kuperberg, Laureline Pinault, Damien Pous. Cyclic Proofs and Jumping Automata. FSTTCS, Dec 2019, Bombay, India. ⟨10.4230/LIPIcs.FSTTCS.2019.45⟩. ⟨hal-02301651v2⟩

Damien Pous. Coinduction: Automata, Formal Proof, Companions (Invited Paper). CALCO, Jun 2019, London, United Kingdom. ⟨hal-02393982⟩

Florent Bréhard, Assia Mahboubi, Damien Pous. A certificate-based approach to formally verified approximations. ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.1-19, ⟨10.4230/LIPIcs.ITP.2019.8⟩. ⟨hal-02088529v2⟩

Amina Doumane, Denis Kuperberg, Damien Pous, Pierre Pradic. Kleene Algebra with Hypotheses. 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), 2019, Prague, Czech Republic. ⟨hal-02021315⟩

Denis Kuperberg, Laureline Pinault, Damien Pous. Coinductive algorithms for Büchi automata. Developments in Language Theory, Aug 2019, Varsovie, Poland. ⟨hal-01928701⟩

Amina Doumane, Damien Pous. Completeness for Identity-free Kleene Lattices. CONCUR, Sep 2018, Beijing, China. ⟨10.4230/LIPIcs.CONCUR.2018.18⟩. ⟨hal-01780845v2⟩

Anupam Das, Damien Pous. Non-wellfounded proof theory for (Kleene+action)(algebras+lattices). Computer Science Logic (CSL), Sep 2018, Birmingham, United Kingdom. ⟨10.4230/LIPIcs.CSL.2018.19⟩. ⟨hal-01703942v3⟩

Damien Pous, Valeria Vignudelli. Allegories: decidability and graph homomorphisms. Logic in Computer Science, Jul 2018, Oxford, United Kingdom. ⟨10.1145/3209108.3209172⟩. ⟨hal-01703906v2⟩

Damien Pous. On the Positive Calculus of Relations with Transitive Closure. 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018), Feb 2018, Caen, France. ⟨10.4230/LIPIcs.STACS.2018.3⟩. ⟨hal-01718925⟩

Christian Doczkal, Damien Pous. Treewidth-Two Graphs as a Free Algebra. Mathematical Foundations of Computer Science, Aug 2018, Liverpool, United Kingdom. ⟨10.4230/LIPIcs.MFCS.2018.60⟩. ⟨hal-01780844v3⟩

Christian Doczkal, Guillaume Combette, Damien Pous. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. ⟨10.1007/978-3-319-94821-8_11⟩. ⟨hal-01703922v2⟩

Anupam Das, Amina Doumane, Damien Pous. Left-Handed Completeness for Kleene algebra, via Cyclic Proofs. LPAR-22, Nov 2018, Awassa, Ethiopia. ⟨hal-01940378⟩

Paul Brunet, Damien Pous, Georg Struth. On Decidability of Concurrent Kleene Algebra. CONCUR, Sep 2017, Berlin, Germany. ⟨hal-01558108⟩

Anupam Das, Damien Pous. A cut-free cyclic proof system for Kleene algebra. TABLEAUX, Sep 2017, Brasilia, Brazil. ⟨hal-01558132⟩

Enric Cosme-Llópez, Damien Pous. K4-free Graphs as a Free Algebra. 42nd International Symposium on Mathematical Foundations of Computer Science, Aug 2017, Aalborg, Denmark. ⟨hal-01515752v2⟩

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, et al.. Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines. LICS 2017, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩. ⟨hal-01479035⟩

Henning Basold, Damien Pous, Jurriaan Rot. Monoidal Company for Accessible Functors. CALCO, Jun 2017, Ljubljana, Slovenia. ⟨hal-01529340⟩

Damien Pous, Jurriaan Rot. Companions, Codensity and Causality. FoSSaCS, Apr 2017, Uppsala, Sweden. ⟨hal-01442222⟩

Paul Brunet, Damien Pous. A formal exploration of Nominal Kleene Algebra. MFCS, Aug 2016, Cracovie, Poland. ⟨10.4230/LIPIcs.MFCS.2016.22⟩. ⟨hal-01307532v2⟩

Paul Brunet, Damien Pous, Insa Stucke. Cardinalities of Finite Relations in Coq with Applications. Interative Theorem Proving, Aug 2016, Nancy, France. pp.466-474, ⟨10.1007/978-3-319-43144-4_29⟩. ⟨hal-01441262v2⟩

Damien Pous. Coinduction All the Way Up. Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), Jul 2016, New York, United States. ⟨10.1145/2933575.2934564⟩. ⟨hal-01259622v2⟩

Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Jean-Claude Reynaud, Damien Pous. Hilbert-Post completeness for the state and the exception effects. Sixth International Conference on Mathematical Aspects of Computer and Information Sciences, Nov 2015, Berlin, Germany. pp.596-610, ⟨10.1007/978-3-319-32859-1_51⟩. ⟨hal-01121924v3⟩

Paul Brunet, Damien Pous. Petri automata for Kleene allegories. Logic in Computer Science, Jul 2015, Kyoto, Japan. pp.68-79, ⟨10.1109/LICS.2015.17⟩. ⟨hal-01073936v3⟩

Damien Pous. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. ⟨hal-01021497v2⟩

Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. 26th International Conference on Concurrency Theory (CONCUR), Sep 2015, Madrid, Spain. ⟨10.4230/LIPIcs.CONCUR.2015.240⟩. ⟨hal-01285299⟩

Damien Pous. Coinductive techniques, from automata to coalgebra. Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India. ⟨10.1145/2792434.2792440⟩. ⟨hal-01288791⟩

Paul Brunet, Damien Pous. Decidability of Identity-free Relational Kleene Lattices. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099137⟩

Paul Brunet, Damien Pous. Kleene Algebra with Converse. RAMiCS, Apr 2014, Marienstatt im Westerwald, Germany. pp.101-118. ⟨hal-00938235⟩

Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous. Formal verification in Coq of program properties involving the global state effect. JFLA 2014 - Journées Francophones des Langages Applicatifs, Jan 2014, Fréjus, France. pp.1-17. ⟨hal-00869230v2⟩

Damien Pous, Alan Schmitt. De la KAM avec un Processus d'Ordre Supérieur. JFLAs 2014, Jan 2014, Fréjus, France. pp.1-12. ⟨hal-00966097v2⟩

Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot. Coinduction up to in a fibrational setting. CSL-LICS, Jul 2014, Vienne, Austria. pp.1-12, ⟨10.1145/2603088.2603149⟩. ⟨hal-00936488v2⟩

Jean-Marie Madiot, Damien Pous, Davide Sangiorgi. Bisimulations up-to: beyond first-order transition systems. CONCUR, Sep 2014, Rome, Italy. ⟨10.1007/978-3-662-44584-6_8⟩. ⟨hal-00990859⟩

Damien Pous. Kleene Algebra with Tests and Coq Tools for While Programs. Interactive Theorem Proving 2013, Jul 2013, Rennes, France. pp.180-196, ⟨10.1007/978-3-642-39634-2_15⟩. ⟨hal-00785969⟩

Filippo Bonchi, Damien Pous. Checking NFA equivalence with bisimulations up to congruence. Principle of Programming Languages (POPL), Jan 2013, Roma, Italy. pp.457-468, ⟨10.1145/2429069.2429124⟩. ⟨hal-00639716v5⟩

Filippo Bonchi, Georgiana Caltais, Damien Pous, Alexandra Silva. Brzozowski's and Up-To Algorithms for Must Testing. 11th Asian Symposium on Programming Languages and Systems (APLAS), Dec 2013, Melbourne, Australia. pp.1-16, ⟨10.1007/978-3-319-03542-0_1⟩. ⟨hal-00966072⟩

Damien Pous. Coalgebraic Up-to Techniques. CALCO, Sep 2013, Warsaw, Poland. ⟨10.1007/978-3-642-40206-7_4⟩. ⟨hal-00966075⟩

Fabienne Boyer, Olivier Gruber, Damien Pous. Robust reconfigurations of component assemblies. ICSE '13 - International Conference on Software Engineering, May 2013, San Francisco, United States. pp.13-22. ⟨hal-00966078⟩

Tom Hirschowitz, Damien Pous. Innocent strategies as presheaves and interactive equivalences for CCS. ICE, Jun 2011, Reykjavik, Iceland. pp.2-24, ⟨10.4204/EPTCS.59.2⟩. ⟨hal-00616648⟩

Thomas Braibant, Damien Pous. Tactics for Reasoning modulo AC in Coq. Certified Proofs and Programs, 2011, Taiwan. pp167-182, ⟨10.1007/978-3-642-25379-9_14⟩. ⟨hal-00484871v4⟩

Damien Pous. Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic. Computer Science Logic, Aug 2010, Brno, Czech Republic. pp.484-498, ⟨10.1007/978-3-642-15205-4_37⟩. ⟨hal-00421158v4⟩

Daniel Hirschkoff, Damien Pous. On Bisimilarity and Substitution in Presence of Replication. ICALP, Jul 2010, Bordeaux, France. pp.454-465, ⟨10.1007/978-3-642-14162-1_38⟩. ⟨hal-00375604v4⟩

Thomas Braibant, Damien Pous. Deciding Kleene Algebras in Coq. ITP, Aug 2010, Edinburgh, United Kingdom. pp.163-178, ⟨10.1007/978-3-642-14052-5_13⟩. ⟨hal-00383070v5⟩

Daniel Hirschkoff, Aurélien Pardon, Tom Hirschowitz, Samuel Hym, Damien Pous. Encapsulation and Dynamic Modularity in the Pi-Calculus. PLACES 2008, 2008, Oslo, Norway. pp.85 - 100, ⟨10.1016/j.entcs.2009.06.005⟩. ⟨hal-00400159⟩

Daniel Hirschkoff, Damien Pous. A Distribution Law for CCS and a New Congruence Result for the pi-calculus. FoSSaCS, 2007, Braga, Portugal. ⟨10.1007/978-3-540-71389-0_17⟩. ⟨hal-00089219v4⟩

Damien Pous. Complete Lattices and Up-to Techniques. 5th Asian Symposium on Programming Languages and Systems, Joxan Jaffar, 2007, Singapore, Singapore. pp.351-366, ⟨10.1007/978-3-540-76637-7_24⟩. ⟨ensl-00155308v2⟩

Damien Pous. On Bisimulation Proofs for the Analysis of Distributed Abstract Machines. TGC, 2006, Lucca, Italy. ⟨10.1007/978-3-540-75336-0_10⟩. ⟨hal-01441457⟩

Damien Pous. Weak Bisimulation Up to Elaboration. CONCUR, 2006, Bonn, Germany. pp.390 - 405, ⟨10.1007/11817949_26⟩. ⟨hal-01441462⟩

Damien Pous. Up-to Techniques for Weak Bisimulation. ICALP, 2005, Lisbonne, Portugal. pp.730 - 741, ⟨10.1007/11523468_59⟩. ⟨hal-01441463⟩

Daniel Hirschkoff, Damien Pous, Davide Sangiorgi. A Correct Abstract Machine for Safe Ambients. COORDINATION, 2005, Namur, Belgium. ⟨10.1007/11417019_2⟩. ⟨hal-01441466⟩

Daniel Hirschkoff, Tom Hirschowitz, Damien Pous, Alan Schmitt, Jean-Bernard Stefani. Component-Oriented Programming with Sharing: Containment is not Ownership. Generative Programming and Component Engineering (GPCE), 2005, Tallinn, Estonia. pp.389-404, ⟨10.1007/11561347_26⟩. ⟨hal-00310126⟩

Damien Pous, Davide Sangiorgi. Enhancements of the bisimulation proof method. Davide Sangiorgi and Jan Rutten. Advanced Topics in Bisimulation and Coinduction, Cambridge University Press, 2012. ⟨hal-00909391⟩

Peter Höfner, Damien Pous, Georg Struth. Relational and algebraic methods in computer science. Journal of Logical and Algebraic Methods in Programming, 106, pp.198-199, 2019, ⟨10.1016/j.jlamp.2019.05.005⟩. ⟨hal-02331045⟩

Peter Höfner, Damien Pous, Georg Struth. 16th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), Proceedings. Peter Hôfner, Damien Pous, Georg Struth. 16th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), 2017, Lyon, France. 10226, Springer, 2017, Proceedings of RAMiCS 2017. ⟨hal-02147353⟩

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, et al.. Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines. [Research Report] RR-9052, Inria. 2017. ⟨hal-01507625⟩

Paul Brunet, Damien Pous. Decidability of Identity-free Relational Kleene Lattices. [Research Report] ENS de Lyon. 2014. ⟨hal-01073932⟩

Damien Pous. Techniques modulo pour les bisimulations. Informatique [cs]. ENS Lyon, 2008. Français. ⟨tel-01441480⟩

Damien Pous. Automata for relation algebra and formal proofs. Computer Science [cs]. ENS Lyon, 2016. ⟨tel-01445821⟩