Production

Publications



212 documents

Journal articles

  • 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⟩
  • 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⟩
  • 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⟩
  • Raphaël Berthon, Nathanaël Fijalkow, Emmanuel Filiot, Shibashis Guha, Bastien Maubert, et al.. Alternating Tree Automata with Qualitative Semantics. ACM Transactions on Computational Logic, Association for Computing Machinery, 2020, 22 (1), ⟨10.1007/s00037-021-00214-1⟩. ⟨hal-02533936⟩
  • Russ Harmer, Eugenia Oshurko. Reversibility and composition of rewriting in hierarchies. EPTCS, 2020. ⟨hal-02869865v2⟩
  • Russ Harmer, Eugenia Oshurko. Knowledge representation and update in hierarchies of graphs. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2020, 114, pp.100559. ⟨10.1016/j.jlamp.2020.100559⟩. ⟨hal-02869805⟩
  • Olivier Laurent. Polynomial time in untyped elementary linear logic. Theoretical Computer Science, Elsevier, 2020, 813, pp.117-142. ⟨10.1016/j.tcs.2019.10.002⟩. ⟨hal-02333452⟩
  • 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⟩
  • Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi. Towards 'up to context' reasoning about higher-order processes. Theoretical Computer Science, Elsevier, 2020, 807, pp.154-168. ⟨10.1016/j.tcs.2019.09.036⟩. ⟨hal-01857391⟩
  • Pierre Clairambault, Marc de Visme. Full abstraction for the quantum lambda-calculus. Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-28. ⟨10.1145/3371131⟩. ⟨hal-02863835⟩
  • 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⟩
  • Patrick Baillot, Gilles Barthe, Ugo Dal Lago. Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. Journal of Automated Reasoning, Springer Verlag, 2019, 63 (4), pp.813-855. ⟨10.1007/978-3-662-48899-7_15⟩. ⟨hal-01197456v3⟩
  • 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⟩
  • Russ Harmer, Yves-Stan Le Cornec, Sébastien Légaré, Eugenia Oshurko. Bio-curation for cellular signalling: the KAMI project. IEEE/ACM Transactions on Computational Biology and Bioinformatics, Institute of Electrical and Electronics Engineers, 2019, 16 (5), pp.1562-1573. ⟨10.1109/TCBB.2019.2906164⟩. ⟨hal-02127147⟩
  • Simon Castellan, Pierre Clairambault, Glynn Winskel. Thin Games with Symmetry and Concurrent Hyland-Ong Games. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, ⟨10.2168/LMCS-15(1:18)2019⟩. ⟨hal-01068769v4⟩
  • Pierre Clairambault, Marc de Visme, Glynn Winskel. Game semantics for quantum programming. Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (POPL), pp.1-29. ⟨10.1145/3290345⟩. ⟨hal-02112184⟩
  • Matthieu Perrinel. Paths-based criteria and application to linear logic subsystems characterizing polynomial time. Information and Computation, Elsevier, 2018, 261, pp.23-54. ⟨10.1016/j.ic.2018.05.004⟩. ⟨hal-02154716⟩
  • Florent Bréhard, Nicolas Brisebarre, Mioara Joldes. Validated and numerically efficient Chebyshev spectral methods for linear ordinary differential equations. ACM Transactions on Mathematical Software, Association for Computing Machinery, 2018, 44 (4), pp.44:1-44:42. ⟨10.1145/3208103⟩. ⟨hal-01526272v3⟩
  • Patrick Baillot, Erika de Benedetti, Simona Ronchi Della Rocca. Characterizing polynomial and exponential complexity classes in elementary lambda-calculus.. Information and Computation, Elsevier, 2018, 248, pp.55-77. ⟨hal-01948275⟩
  • Matteo Mio, Micha Skrzypczak, Henryk Michalewski. Monadic Second Order Logic with Measure and Category Quantifiers. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2018, 14, pp.1 - 29. ⟨10.23638/LMCS-14(2:2)2018⟩. ⟨hal-01872169⟩
  • Javier Esparza, Denis Kuperberg, Anca Muscholl, Igor Walukiewicz. Soundness in negotiations. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2018, ⟨10.4230/LIPIcs⟩. ⟨hal-01891179⟩
  • Pierre Clairambault, Charles Grellois, Andrzej Murawski. Linearity in higher-order recursion schemes. Proceedings of the ACM on Programming Languages, ACM, 2017, 2, pp.1 - 29. ⟨10.1145/3158127⟩. ⟨hal-01886931⟩
  • Simon Castellan, Pierre Clairambault, Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended Version). Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, ⟨10.23638/LMCS-13(4:22)2017⟩. ⟨hal-01579415⟩
  • Tomasz Gogacz, Henryk Michalewski, Matteo Mio, Michał Skrzypczak. Measure properties of regular sets of trees. Information and Computation, Elsevier, 2017, 256, pp.108 - 130. ⟨10.1016/j.ic.2017.04.012⟩. ⟨hal-01872157⟩
  • Simon Castellan, Pierre Clairambault, Silvain Rideau, Glynn Winskel. Games and Strategies as Event Structures. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, ⟨10.23638/LMCS-13(3:35)2017⟩. ⟨hal-01302713v3⟩
  • 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⟩
  • Olivier Laurent. Focusing in Orthologic. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (3), pp.6. ⟨10.23638/LMCS-13(3:6)2017⟩. ⟨hal-01566869⟩
  • Matteo Mio, Alex Simpson. Łukasiewicz μ-calculus. Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2017, 150 (3-4), pp.317 - 346. ⟨10.3233/FI-2017-1472⟩. ⟨hal-01903167⟩
  • Anupam Das, Lutz Straßburger. On linear rewriting systems for Boolean logic and some applications to proof theory. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016. ⟨hal-01422611⟩
  • 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⟩
  • Daniel Hirschkoff, Jean-Marie Madiot, Davide Sangiorgi. Name-passing calculi: From fusions to preorders and types. Information and Computation, Elsevier, 2016, 251, pp.26. ⟨10.1016/j.ic.2016.10.003⟩. ⟨hal-01419632⟩
  • Patrick Baillot, Ugo Dal Lago. Higher-order interpretations and program complexity. Information and Computation, Elsevier, 2016, ⟨10.1016/j.ic.2015.12.008⟩. ⟨hal-01337728⟩
  • 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⟩
  • Patrick Baillot. On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy.. Information and Computation, Elsevier, 2015, 241, pp.3-31. ⟨hal-01948302⟩
  • 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⟩
  • Vincent Danos, Russell Harmer, Ricardo Honorato-Zimmer, Hernán Melgratti. Thermodynamic graph-rewriting. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 11 (2), ⟨10.2168/LMCS-11(2:13)2015⟩. ⟨hal-01974698⟩
  • Pierre Clairambault. Bounding Linear Head Reduction and Visible Interaction Through Skeletons. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 11 (2), pp.6. ⟨10.2168/LMCS-11(2:6)2015⟩. ⟨hal-01286473⟩
  • Pierre Clairambault, Peter Dybjer. The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2014, 24 (05), pp.e240501. ⟨10.1017/S0960129513000881⟩. ⟨hal-00990027⟩
  • Vincent Danos, Russell Harmer, Ricardo Honorato-Zimmer. Thermodynamic graph-rewriting. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 11 (2), pp.13. ⟨10.2168/LMCS-11(2:13)2015⟩. ⟨hal-01263637⟩
  • Pierre Lescanne, Katarzyna Grygiel. Counting and generating lambda terms. Journal of Functional Programming, Cambridge University Press (CUP), 2013, 23 (05), pp.594-628. ⟨10.1017/S0956796813000178⟩. ⟨ensl-00879067⟩
  • Vincent Danos, Russ Harmer, Glynn Winskel. Constraining rule-based dynamics with types. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (02), pp.272-289. ⟨hal-01976370⟩
  • Olivier Laurent. Intersection Types with Subtyping by Means of Cut Elimination. Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2012, 121 (1-4), pp.203-226. ⟨10.3233/FI-2012-776⟩. ⟨hal-00768868⟩
  • 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⟩
  • Daniel Hirschkoff, Jean-Marie Madiot, Davide Sangiorgi. Duality and i/o-Types in the π-Calculus. Lecture Notes in Computer Science, Springer, 2012, 7454, pp 302-316. ⟨hal-00798028⟩
  • 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⟩
  • Olivier Laurent. Intuitionistic Dual-intuitionistic Nets. Journal of Logic and Computation, Oxford University Press (OUP), 2011, 21 (4), pp.561-587. ⟨10.1093/logcom/exp044⟩. ⟨hal-00617254⟩
  • Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi. Termination in higher-order concurrent calculi. Journal of Logic and Algebraic Programming, Elsevier, 2010, 79 (7), pp.550-577. ⟨10.1016/j.jlap.2010.07.007⟩. ⟨hal-00798788⟩
  • 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, 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. 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⟩

Conference papers

  • 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. ⟨hal-03269462v2⟩
  • Lison Blondeau-Patissier, Pierre Clairambault. Positional Injectivity for Innocent Strategies. 6TH INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION, Jul 2021, Buenos Aires, Argentina. ⟨hal-03218198⟩
  • Denis Kuperberg. Positive First-order Logic on Words. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, France. pp.1-13, ⟨10.1109/LICS52264.2021.9470602⟩. ⟨hal-03375096⟩
  • Etienne Callies, Olivier Laurent. Click and coLLecT An Interactive Linear Logic Prover. 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy. ⟨lirmm-03271501⟩
  • Russ Harmer, Nicolas Behr, Jean Krivine. Concurrency Theorems for Non-linear Rewriting Theories. ICGT 2021 - 14th International Conference on Graph Transformation, Jun 2021, Bergen, Norway. pp.3-21, ⟨10.1007/978-3-030-78946-6_1⟩. ⟨hal-03358036⟩
  • Patrick Baillot, Alexis Ghyselen. Types for Complexity of Parallel Computation in Pi-Calculus. 30th European Symposium on Programming (ESOP 2021), Mar 2021, Luxembourg, Luxembourg. pp.59-86. ⟨hal-03126973⟩
  • Hanâ Lbath, Angela Bonifati, Russ Harmer. Schema Inference for Property Graphs. EDBT 2021 - 24th International Conference on Extending Database Technology, Mar 2021, Nicosia, Cyprus. pp.499-504, ⟨10.5441/002/edbt.2021.58⟩. ⟨hal-03361480⟩
  • Bruno Dinis, Étienne Miquey. Realizability with stateful computations for nonstandard analysis. CSL 2021 - Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨hal-03002239⟩
  • Olivier Laurent. An Anti-Locally-Nameless Approach to Formalizing Quantifiers. Certified Programs and Proofs, Jan 2021, virtual, Denmark. pp.300-312, ⟨10.1145/3437992.3439926⟩. ⟨hal-03096253⟩
  • Udi Boker, Denis Kuperberg, Karoliina Lehtinen, Michał Skrzypczak. On the Succinctness of Alternating Parity Good-for-Games Automata. FSTTCS 2020, Dec 2020, Goa, India. pp.41:1--41:13. ⟨hal-03046213⟩
  • 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⟩
  • Denis Kuperberg, Laureline Pinault, Damien Pous. Cyclic Proofs and Jumping Automata. FSTTCS, Dec 2019, Bombay, India. ⟨10.4230/LIPIcs.FSTTCS.2019.45⟩. ⟨hal-02301651v2⟩
  • Angela Bonifati, Peter Furniss, Alastair Green, Russ Harmer, Eugenia Oshurko, et al.. Schema validation and evolution for graph databases. ER 2019 - 38th International Conference on Conceptual Modeling, Nov 2019, Salvador, Brazil. pp.448-456, ⟨10.1007/978-3-030-33223-5_37⟩. ⟨hal-02138771⟩
  • Russ Harmer, Eugenia Oshurko. KAMIStudio: an environment for biocuration of cell signalling knowledge. 17th International Conference on Computational Methods in Systems Biology, Sep 2019, Trieste, Italy. ⟨hal-02138766⟩
  • 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⟩
  • Pierre Clairambault, Andrzej Murawski. On the Expressivity of Linear Recursion Schemes. 44th International Symposium on Mathematical Foundations of Computer Science, Aug 2019, Aachen, Germany. ⟨10.4230/LIPIcs.MFCS.2019.50⟩. ⟨hal-02313542⟩
  • Marc de Visme. Event structures for mixed choice. The 30th International Conference on Concurrency Theory, CONCUR 2019, Aug 2019, Amsterdam, Netherlands. ⟨hal-02167420⟩
  • Simon Iosti, Denis Kuperberg. Eventually Safe Languages. Developments in Language Theory, Aug 2019, Varsovie, Poland. pp.192-205, ⟨10.1007/978-3-030-24886-4_14⟩. ⟨hal-02348828⟩
  • Denis Kuperberg, Laureline Pinault, Damien Pous. Coinductive algorithms for Büchi automata. Developments in Language Theory, Aug 2019, Varsovie, Poland. ⟨hal-01928701⟩
  • Russ Harmer, Eugenia Oshurko. Knowledge representation and update in hierarchies of graphs. International Conference on Graph Transformation, Jul 2019, Eindhoven, Netherlands. ⟨hal-02127178⟩
  • Florent Bréhard, Mioara Joldes, Jean-Bernard Lasserre. On Moment Problems with Holonomic Functions. 44th International Symposium on Symbolic and Algebraic Computation (ISSAC 2019), Jul 2019, Pékin, China. pp.66-73. ⟨hal-02006645⟩
  • Lê Thành Dũng Nguyễn, Pierre Pradic. From normal functors to logarithmic space queries. 46th International Colloquium on Automata, Languages and Programming (ICALP 2019), Jul 2019, Patras, Greece. ⟨10.4230/LIPIcs.ICALP.2019.123⟩. ⟨hal-02024152v2⟩
  • Denis Arzelier, Florent Bréhard, Mioara Joldes. Exchange algorithm for evaluation and approximation error-optimized polynomials. ARITH 2019 - 26th IEEE Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.1-8. ⟨hal-02006606⟩
  • Damien Pous. Coinduction: Automata, Formal Proof, Companions (Invited Paper). CALCO, Jun 2019, London, United Kingdom. ⟨hal-02393982⟩
  • Aurore Alcolei, Pierre Clairambault, Olivier Laurent. Resource-Tracking Concurrent Games. Foundations of Software Science and Computation Structures, Apr 2019, Prague, Czech Republic. pp.27-44, ⟨10.1007/978-3-030-17127-8_2⟩. ⟨hal-02096306⟩
  • Christophe Lucas, Matteo Mio. Towards a Structural Proof Theory of Probabilistic mu-Calculi. FoSSaCS, Apr 2019, Prague, Czech Republic. pp.418-435. ⟨hal-02136732⟩
  • Pierre Pradic, Colin Riba. A Dialectica-Like Interpretation of a Linear MSO on Infinite Words. FOSSACS'19, Apr 2019, Prague, Czech Republic. ⟨hal-01925701⟩
  • 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⟩
  • Anupam Das, Amina Doumane, Damien Pous. Left-Handed Completeness for Kleene algebra, via Cyclic Proofs. LPAR-22, Nov 2018, Awassa, Ethiopia. ⟨hal-01940378⟩
  • Romain Serra, Denis Arzelier, Florent Bréhard, Mioara Joldes. Fuel-optimal impulsive fixed-time trajectories in the linearized circular restricted 3-body-problem. IAC 2018 - 69th International Astronautical Congress; IAF Astrodynamics Symposium, International Astronautical Federation, Oct 2018, Bremen, Germany. pp.1-9. ⟨hal-01830253⟩
  • Patrick Baillot, Alexis Ghyselen. Combining Linear Logic and Size Types for Implicit Complexity. Conference on Computer Science Logic, CSL 2018, Sep 2018, Birmingham, France. pp.9:1--9:21. ⟨hal-01948196⟩
  • 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⟩
  • Pierre Clairambault, Hugo Paquet. Fully Abstract Models of the Probabilistic λ-calculus. 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Sep 2018, Birmingham, United Kingdom. ⟨10.4230/LIPIcs.CSL.2018.16⟩. ⟨hal-01886956⟩
  • Aurore Alcolei, Pierre Clairambault, Martin Hyland, Glynn Winskel. The True Concurrency of Herbrand’s Theorem. 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Sep 2018, Birmingham, United Kingdom. ⟨10.4230/LIPIcs.CSL.2018.5⟩. ⟨hal-01886968⟩
  • Amina Doumane, Damien Pous. Completeness for Identity-free Kleene Lattices. CONCUR, Sep 2018, Beijing, China. ⟨10.4230/LIPIcs.CONCUR.2018.18⟩. ⟨hal-01780845v2⟩
  • 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⟩
  • Florent Bréhard. A Newton-like Validation Method for Chebyshev Approximate Solutions of Linear Ordinary Differential Systems. ISSAC 2018 - 43rd International Symposium on Symbolic and Algebraic Computation, Jul 2018, New York, United States. pp.103-110, ⟨10.1145/3208976.3209000⟩. ⟨hal-01654396v2⟩
  • Simon Castellan, Pierre Clairambault, Hugo Paquet, Glynn Winskel. The concurrent game semantics of Probabilistic PCF. the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), Jul 2018, Oxford, France. ⟨10.1145/3209108.3209187⟩. ⟨hal-01886965⟩
  • Pierre Pradic, Colin Riba. LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic. LICS'18, Jul 2018, Oxford, United Kingdom. ⟨hal-01698648v2⟩
  • Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi. Eager Functions as Processes. the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2018, Oxford, United Kingdom. ⟨10.1145/3209108.3209152⟩. ⟨hal-01917255⟩
  • Olivier Laurent. Around Classical and Intuitionistic Linear Logics. the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. ⟨10.1145/3209108.3209132⟩. ⟨hal-01840882⟩
  • Matteo Mio. Riesz Modal Logic with Threshold Operators. the 33rd Annual ACM/IEEE Symposium, Jul 2018, Oxford, France. ⟨10.1145/3209108.3209118⟩. ⟨hal-01872130⟩
  • Olivier Laurent. Intersection Subtyping with Constructors. Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems, Jul 2018, Oxford, United Kingdom. pp.73-84, ⟨10.4204/EPTCS.293.6⟩. ⟨hal-02159762⟩
  • Damien Pous, Valeria Vignudelli. Allegories: decidability and graph homomorphisms. Logic in Computer Science, Jul 2018, Oxford, United Kingdom. ⟨10.1145/3209108.3209172⟩. ⟨hal-01703906v2⟩
  • 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⟩
  • Guilhem Jaber, Nikos Tzevelekos. A Trace Semantics for System F Parametric Polymorphism. International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessaloniki, Greece. pp.20-38, ⟨10.1007/978-3-319-89366-2_2⟩. ⟨hal-02083207⟩
  • Simon Castellan, Pierre Clairambault, Jonathan Hayman, Glynn Winskel. Non-angelic Concurrent Game Semantics. 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018), Apr 2018, Thessaloniki, Greece. ⟨10.1007/978-3-319-89366-2_1⟩. ⟨hal-01886951⟩
  • 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⟩
  • Paulo Ricardo Arantes Gilz, Florent Bréhard, Clément Gazzino. Validated Semi-Analytical Transition Matrices for Linearized Relative Spacecraft Dynamics via Chebyshev Series Approximations. SCITECH 2018 - AIAA Science and Technology Forum and Exposition, 28th Space Flight Mechanics Meeting, Jan 2018, Kissimmee, United States. pp.1-23, ⟨10.2514/6.2018-1960⟩. ⟨hal-01540170v3⟩
  • Denis Kuperberg, Anirban Majumdar. Width of Non-deterministic Automata. 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018), 2018, Caen, France. pp.48 - 49, ⟨10.4230/LIPIcs.STACS.2018.48⟩. ⟨hal-01891180⟩
  • Russ Harmer, Yves-Stan Le Cornec, Sébastien Légaré, Ievgeniia Oshurko. Bio-curation for cellular signalling: the KAMI project. Computational Methods in Systems Biology, Sep 2017, Darmstadt, Germany. ⟨10.1007/978-3-319-67471-1_1⟩. ⟨hal-01617185⟩
  • Anupam Das, Damien Pous. A cut-free cyclic proof system for Kleene algebra. TABLEAUX, Sep 2017, Brasilia, Brazil. ⟨hal-01558132⟩
  • Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi. Divergence and unique solution of equations. CONCUR 2017 - 28th International Conference on Concurrency Theory, Sep 2017, Berlin, Germany. pp.1 - 7, ⟨10.4230/LIPIcs.CONCUR.2017.7⟩. ⟨hal-01643502⟩
  • Paul Brunet, Damien Pous, Georg Struth. On Decidability of Concurrent Kleene Algebra. CONCUR, Sep 2017, Berlin, Germany. ⟨hal-01558108⟩
  • Simon Castellan, Pierre Clairambault, Glynn Winskel. Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or. Second International Conference on Formal Structures for Computation and Deduction, FSCD 2017, Sep 2017, Oxford, United Kingdom. pp.1 - 12, ⟨10.4230/LIPIcs.FSCD.2017.12⟩. ⟨hal-01886926⟩
  • Pierre Pradic, Colin Riba. A Curry-Howard Approach to Church's Synthesis. FSCD'17, Sep 2017, Oxford, United Kingdom. ⟨10.4230/LIPIcs.FSCD.2017.29⟩. ⟨hal-01511837v2⟩
  • 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⟩
  • Simon Castellan, Pierre Clairambault, Glynn Winskel. Distributed Strategies Made Easy. 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, Aug 2017, Aalborg, Denmark. ⟨10.4230/LIPIcs.MFCS.2017.81⟩. ⟨hal-01886946⟩
  • Matteo Mio, Robert Furber, Radu Mardare. Riesz Modal logic for Markov processes. 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2017, Reykjavik, France. ⟨10.1109/LICS.2017.8005091⟩. ⟨hal-01872150⟩
  • Henning Basold, Damien Pous, Jurriaan Rot. Monoidal Company for Accessible Functors. CALCO, Jun 2017, Ljubljana, Slovenia. ⟨hal-01529340⟩
  • 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⟩
  • Damien Pous, Jurriaan Rot. Companions, Codensity and Causality. FoSSaCS, Apr 2017, Uppsala, Sweden. ⟨hal-01442222⟩
  • Nathanaël Fijalkow, Hugo Gimbert, Edon Kelmendi, Denis Kuperberg. Stamina: Stabilisation Monoids IN Automata theory. CIAA - International Conference on Implementation and Application of Automata, 2017, Marne-la-Vallée, France. ⟨hal-01891164⟩
  • Patrick Baillot, Anupam Das. Free-cut elimination in linear logic and an application to a feasible arithmetic . Computer Science Logic 2016, Aug 2016, Marseille, France. pp. 40:1-40:18, ⟨10.4230/LIPIcs.CSL.2016.40⟩. ⟨hal-01316754⟩
  • Simon Castellan, Pierre Clairambault. Causality vs. interleavings in concurrent game semantics. The 27th International Conference on Concurrency Theory (CONCUR 2016), Aug 2016, Québec City, Canada. pp.1 - 3214, ⟨10.4230/LIPIcs.CONCUR.2016.32⟩. ⟨hal-01474550⟩
  • 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⟩
  • Paul Brunet, Damien Pous. A formal exploration of Nominal Kleene Algebra. MFCS, Aug 2016, Cracovie, Poland. ⟨10.4230/LIPIcs.MFCS.2016.22⟩. ⟨hal-01307532v2⟩
  • 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⟩
  • Olivier Laurent. Focusing in Orthologic. Formal Structures for Computation and Deduction, Jun 2016, Porto, Portugal. pp.25, ⟨10.4230/LIPIcs.FSCD.2016.25⟩. ⟨hal-01306132⟩
  • Laure Daviaud, Denis Kuperberg, Jean-Eric Pin. Varieties of Cost Functions. 33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, Feb 2016, Orléans, France. pp.1-30, ⟨10.4230/LIPIcs.STACS.2016.30⟩. ⟨hal-01614389⟩
  • Laure Daviaud, Pierre-Alain Reynier, Jean-Marc Talbot. A Generalized Twinning Property for Minimisation of Cost Register Automata. Proc. 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'16), 2016, Unknown, Unknown Region. pp.857--866, ⟨10.1145/2933575.2934549⟩. ⟨hal-01475441⟩
  • Henryk Michalewski, Matteo Mio. On the Problem of Computing the Probability of Regular Sets of Trees. Proc. of FSTTCS 2015, Dec 2015, Bangalore, India. pp.489 - 502, ⟨10.4230/LIPIcs.FSTTCS.2015.489⟩. ⟨hal-02140487⟩
  • Patrick Baillot, Gilles Barthe, Ugo Dal Lago. Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs.. Logic for Programming, Artificial Intelligence, and Reasoning - 20thInternational Conference, LPAR-20, Nov 2015, Suva, Fiji. pp.203-218. ⟨hal-01948334⟩
  • 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⟩
  • Adrien Basso-Blandin, Walter Fontana, Russ Harmer. A knowledge representation meta-model for rule-based modelling of signalling networks. DCM, Oct 2015, Cali, Colombia. ⟨10.4204/EPTCS.204.5⟩. ⟨hal-01468117⟩
  • 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⟩
  • Henryk Michalewski, Matteo Mio. Baire Category Quantifier in Monadic Second Order Logic. Proc. of ICALP 2015, Jul 2015, Kyoto, Japan. pp.362-374. ⟨hal-02140480⟩
  • Simon Castellan, Pierre Clairambault, Glynn Winskel. The Parallel Intensionally Fully Abstract Games Model of PCF. Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2015, Kyoto, Japan. ⟨10.1109/LICS.2015.31⟩. ⟨hal-01286477⟩
  • Simon Castellan, Pierre Clairambault, Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. TLCA 2015 13th International Conference on Typed Lambda Calculi and Applications, Jul 2015, Varsovie, Poland. ⟨10.4230/LIPIcs.TLCA.2015.138⟩. ⟨hal-01286479⟩
  • Colin Riba. Fibrations of Tree Automata. TLCA 2015, Jul 2015, Varsovie, Poland. pp.302--316, ⟨10.4230/LIPIcs.TLCA.2015.302⟩. ⟨hal-01261182⟩
  • Daniel Hirschkoff, Jean-Marie Madiot, Xian Xu. A Behavioural Theory for a π-calculus with Preorders. 6th Fundamentals of Software Engineering (FSEN), Apr 2015, Tehran, Iran. pp.143-158, ⟨10.1007/978-3-319-24644-4_10⟩. ⟨hal-01246094v2⟩
  • Pierre Clairambault, Peter Dybjer. Game Semantics and Normalization by Evaluation. 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Apr 2015, Londres, United Kingdom. ⟨10.1007/978-3-662-46678-0_4⟩. ⟨hal-01286469⟩
  • Damien Pous. Coinductive techniques, from automata to coalgebra. Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India. ⟨10.1145/2792434.2792440⟩. ⟨hal-01288791⟩
  • 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⟩
  • 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⟩
  • Simon Castellan, Pierre Clairambault, Glynn Winskel. Symmetry in Concurrent Games. Logic in Computer Science, Jul 2014, Vienna, Austria. 10 p. ⟨hal-00990020⟩
  • 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⟩
  • Katarzyna Grygiel, Pierre Lescanne. Counting Terms in the Binary Lambda Calculus. 25th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms, Jun 2014, Paris, France. pp.13. ⟨ensl-00923203⟩
  • 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⟩
  • Pierre Clairambault, Andrzej Murawski. Böhm trees as higher-order recursion schemes. Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013), Dec 2013, Guwahati, India. pp.91--102, ⟨10.4230/LIPIcs.FSTTCS.2013.91⟩. ⟨hal-00966102⟩
  • 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⟩
  • Valentin Blot, Colin Riba. On Bar Recursion and Choice in a Classical Setting. Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Dec 2013, Melbourne, Australia. pp.349-364, ⟨10.1007/978-3-319-03542-0_25⟩. ⟨hal-00835540⟩
  • Damien Pous. Coalgebraic Up-to Techniques. CALCO, Sep 2013, Warsaw, Poland. ⟨10.1007/978-3-642-40206-7_4⟩. ⟨hal-00966075⟩
  • Matthieu Perrinel. On paths-based criteria for polynomial time complexity in proof-nets. Foundational and Practical Aspects of Resource Analysis (FOPARA) 2013, Aug 2013, Bertinoro, Italy. pp.127--142, ⟨10.1007/978-3-319-12466-7_8⟩. ⟨hal-00992578⟩
  • 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⟩
  • Colin Riba. Forcing MSO on Infinite Words in Weak MSO. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2013, New Orleans, United States. pp.448-457, ⟨10.1109/LICS.2013.51⟩. ⟨hal-00776921v2⟩
  • 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⟩
  • Matteo Mio, Alex Simpson. A Proof System for Compositional Verification of Probabilistic Concurrent Processes. Foundations of Software Science and Computation Structures - 16th International Conference (FOSSACS 2013), Mar 2013, Rome, Italy. pp.161-176. ⟨hal-00766384⟩
  • 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⟩
  • Daniel Hirschkoff, Jean-Marie Madiot, Davide Sangiorgi. Name-passing calculi: from fusions to preorders and types. LICS - 28th Annual ACM/IEEE Symposium on Logic in Computer Science - 2013, 2013, New Orleans, United States. pp.378-387, ⟨10.1109/LICS.2013.44⟩. ⟨hal-00904138⟩
  • Vincent Danos, Russ Harmer, Ricardo Honorato-Zimmer. Thermodynamic graph rewriting. Proceedings of CONCUR 2013, 2013, Buenos-Aires, Argentina. ⟨hal-01974676⟩
  • Colin Riba. A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Streams. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.310-324, ⟨10.1007/978-3-642-33475-7_22⟩. ⟨hal-00692153⟩
  • Daniel Hirschkoff, Jean-Marie Madiot, Davide Sangiorgi. Duality and i/o-Types in the pi-calculus. 23rd International Conference on Concurrency Theory (CONCUR 2012), 2012, Newcastle upon Tyne, United Kingdom. pp.302--316, ⟨10.1007/978-3-642-32940-1_22⟩. ⟨hal-00909375⟩
  • Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi. Termination in impure lambda-calculus. Fundamentals of Software Engineering, 2012, Unknown, Afghanistan. pp.128--142. ⟨hal-00909392⟩
  • 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⟩
  • 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⟩
  • Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi. Termination in Impure Concurrent Languages. CONCUR'10, 2010, Paris, France. pp.328-342, ⟨10.1007/978-3-642-15375-4_23⟩. ⟨hal-00798789⟩
  • Colin Riba. On the Values of Reducibility Candidates. Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Jul 2009, Brasilia, Brazil. pp 264-278, ⟨10.1007/978-3-642-02273-9_20⟩. ⟨hal-00800668⟩
  • 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⟩
  • 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⟩

Poster communications

  • Sébastien Légaré, Jean Krivine, Russ Harmer, Jérôme Feret. Modelling Systems Biology Wide and Deep. CMSB 2021 - 19th International Conference on Computational Methods in Systems Biology, Sep 2021, Bordeaux, France. CMSB. ⟨hal-03357485⟩

Book sections

  • Pierre Clairambault, Simon Castellan, Peter Dybjer. Categories with Families: Unityped, Simply Typed, and Dependently Typed. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, 20, Springer International Publishing, pp.135-180, 2021, Outstanding Contributions to Logic, ⟨10.1007/978-3-030-66545-6_5⟩. ⟨hal-03419296⟩
  • 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⟩

Directions of work or proceedings

  • 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⟩
  • Russ Harmer, Ugo Dal Lago. Special Issue of EPTCS (vol 179) for DCM 2014. 2015. ⟨hal-02132689⟩
  • Ralph Matthes, Matteo Mio. Tenth International Workshop on Fixed Points in Computer Science (FICS 2015), Berlin, Allemagne, 11/09/2015 - 12/09/2015. Matthes, Ralph; Mio, Matteo. Electronic Proceedings in Theoretical Computer Science, 2015, ⟨10.4204/EPTCS.191⟩. ⟨hal-03198240⟩
  • Thomas Ehrhard, Claudia Faggian, Olivier Laurent. Girard's Festschrift, Theoretical Computer Science (Volume 412, Issue 20). Elsevier, pp.240, 2011. ⟨hal-00589711⟩

Preprints, Working Papers

  • Simon Castellan, Pierre Clairambault, Glynn Winskel. The Mays and Musts of Concurrent Strategies. 2021. ⟨hal-03323995⟩
  • Pierre Clairambault, Simon Castellan. The Concurrent Games Abstract Machine: Multi-Token Geometry of Interaction and its Causal Unfolding. 2021. ⟨hal-03286443⟩
  • Pierre Clairambault, Hugo Paquet. The Quantitative Collapse of Concurrent Games with Symmetry. 2021. ⟨hal-03280420⟩
  • Simon Castellan, Pierre Clairambault. Disentangling Parallelism and Interference in Game Semantics. 2021. ⟨hal-03182043⟩
  • Guilhem Jaber, Colin Riba. Temporal Refinements for Guarded Recursive Types. 2021. ⟨hal-02512655v5⟩
  • Anupam Das, Colin Riba. A functional (Monadic) second-order theory of infinite trees. 2020. ⟨hal-02067267v2⟩
  • Pierre Clairambault. Learning to Count up to Symmetry. 2020. ⟨hal-02861005⟩
  • Christian Doczkal, Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. 2019. ⟨hal-02127698⟩
  • Pierre Pradic, Chad Brown. Cantor-Bernstein implies Excluded Middle. 2019. ⟨hal-02103517⟩
  • Christian Doczkal. Short proof of Menger's Theorem in Coq (Proof Pearl). 2019. ⟨hal-02086931⟩
  • Florent Bréhard, Nicolas Brisebarre, Mioara Joldes, Warwick Tucker. A New Lower Bound on the Hilbert Number for Quartic Systems. 2019. ⟨hal-02085895⟩
  • Colin Riba. Monoidal-Closed Categories of Tree Automata. 2018. ⟨hal-01261183v10⟩
  • Colin Riba, Guilhem Jaber. Modal Logic of Transition Systems in the Topos of Trees. 2017. ⟨hal-01620992⟩
  • Daniel Hirschkoff, Jean-Marie Madiot, Xian Xu. A behavioural theory for a π-calculus with preorders. 2014. ⟨hal-00949521⟩
  • Daniel Hirschkoff, Jean-Marie Madiot, Davide Sangiorgi. Name-passing calculi: from fusions to preorders and types. 2013. ⟨hal-00818068v2⟩
  • Katarzyna Grygiel, Pierre Lescanne. Counting and generating lambda terms. 2012. ⟨ensl-00740034v7⟩
  • Colin Riba. On the Representation of Stream Functions in Denotational Domains. 2011. ⟨hal-00617624⟩

Reports

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

Theses

  • Alexis Ghyselen. Sized Types Methods and their Applications to Complexity Analysis in Pi-Calculus. Computational Complexity [cs.CC]. Université de Lyon, 2021. English. ⟨NNT : 2021LYSEN036⟩. ⟨tel-03405961⟩
  • Laureline Pinault. From automata to cyclic proofs : equivalence algorithms and descriptive complexity. Logic in Computer Science [cs.LO]. Université de Lyon, 2021. English. ⟨NNT : 2021LYSEN024⟩. ⟨tel-03412556⟩
  • Marc de Visme. Quantum Game Semantics. Logic in Computer Science [cs.LO]. Université de Lyon, 2020. English. ⟨NNT : 2020LYSEN056⟩. ⟨tel-03045844⟩
  • Ievgeniia Oshurko. Knowledge representation and curation in hierarchies of graphs. Artificial Intelligence [cs.AI]. Université de Lyon, 2020. English. ⟨NNT : 2020LYSEN024⟩. ⟨tel-02917559⟩
  • Pierre Pradic. Some proof-theoretical approaches to Monadic Second-Order logic. Logic in Computer Science [cs.LO]. Université de Lyon; Uniwersytet Warszawski. Wydział Matematyki, Informatyki i Mechanik, 2020. English. ⟨NNT : 2020LYSEN028⟩. ⟨tel-02954006⟩
  • Aurore Alcolei. Enriched concurrent games : witnesses for proofs and resource analysis. Logic in Computer Science [cs.LO]. Université de Lyon; University of Cambridge, 2019. English. ⟨NNT : 2019LYSEN054⟩. ⟨tel-02448974⟩
  • Simon Castellan. Concurrent structures in game semantics. Logic in Computer Science [cs.LO]. Université de Lyon, 2017. English. ⟨NNT : 2017LYSEN034⟩. ⟨tel-01587718⟩
  • Athanasios Tsouanas. On the Semantics of Disjunctive Logic Programs. Logic in Computer Science [cs.LO]. Ecole Nationale Supérieure de Lyon, 2014. English. ⟨tel-02139060⟩
  • Damien Pous. Techniques modulo pour les bisimulations. Informatique [cs]. ENS Lyon, 2008. Français. ⟨tel-01441480⟩

HDR thesis

  • Russell Harmer. Rule-based meta-modelling for bio-curation. Bioinformatics [q-bio.QM]. Ecole Normale Supérieure de Lyon, 2017. ⟨tel-01534703⟩
  • Damien Pous. Automata for relation algebra and formal proofs. Computer Science [cs]. ENS Lyon, 2016. ⟨tel-01445821⟩
  • Olivier Laurent. Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire. Mathématiques [math]. Université Paris-Diderot - Paris VII, 2010. ⟨tel-00460805⟩

Software