Damien Pous

Damien Pous, Denis Kuperberg, Laureline Pinault. Coinductive Algorithms for Büchi Automata. Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2021, 180 (4), pp.351-373. ⟨10.3233/FI-2021-2046⟩. ⟨hal-03364935⟩

Jean-Marie Madiot, Damien Pous, Davide Sangiorgi. Modular coinduction up-to for higher-order languages via first-order transition systems. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2021, Volume 17, Issue 3, ⟨10.46298/lmcs-17(3:25)2021⟩. ⟨hal-03350199⟩

Denis Kuperberg, Laureline Pinault, Damien Pous. Cyclic proofs, system T, and the power of contraction. Proceedings of the ACM on Programming Languages, ACM, 2021, ⟨10.1145/3434282⟩. ⟨hal-02487175v2⟩

Christian Doczkal, Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-020-09543-2⟩. ⟨hal-02316859v2⟩

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⟩

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⟩

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 of the ACM, Association for Computing Machinery, 2015, 58 (2), pp.87-95. ⟨10.1145/2713167⟩. ⟨hal-01284907⟩

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. 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⟩

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⟩

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⟩

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⟩

Damien Pous, Jurriaan Rot, Ruben Turkenburg. Corecursion up-to via Causal Transformations. Coalgebraic Methods in Computer Science, Apr 2022, Munich, Germany. ⟨10.1007/978-3-031-10736-8_7⟩. ⟨hal-03694381⟩

Damien Pous, Jana Wagemaker. Completeness Theorems for Kleene Algebra with Top. CONCUR, Sep 2022, Varsovie, Poland. ⟨10.4230/LIPIcs.CONCUR.2022.26⟩. ⟨hal-03644317v2⟩

Damien Pous, Jurriaan Rot, Jana Wagemaker. On Tools for Completeness of Kleene Algebra with Hypotheses. 19th International Conference on Relational and Algebraic Methods in Computer Science ( RAMICS 2021 ), Nov 2021, Luminy, France. ⟨10.1007/978-3-030-88701-8_23⟩. ⟨hal-03269462v2⟩

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⟩

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⟩

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

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

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

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⟩

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⟩

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⟩

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⟩

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⟩

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⟩

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

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

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

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⟩

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

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

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 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩. ⟨hal-01479035⟩

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

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⟩

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. 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⟩

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⟩

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⟩

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⟩

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⟩

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⟩

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⟩

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

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⟩

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

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. 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⟩

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⟩

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, 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⟩

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, 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⟩

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⟩

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. 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⟩

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. Up-to Techniques for Weak Bisimulation. ICALP, 2005, Lisbonne, Portugal. pp.730 - 741, ⟨10.1007/11523468_59⟩. ⟨hal-01441463⟩

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⟩

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⟩