Colin Riba

Welcome!

I am an assistant professor ("Maître de Conférences (HDR)" in French) in the Computer Science Department of ENS Lyon.
I do my research in the Plume team, at LIP laboratory, also in ENS Lyon.

During year 2008-2009, I was a teaching assistant ("ATER" in Fench) in the same department, doing my research in the same team.
From November 2007 to August 2008, I was a postdoctoral fellow in the Everest project of INRIA Sophia Antipolis.
During 2004-2007, I was a PhD student at LORIA (Laboratoire Lorrain de Recherche en Informatique et ses Applications) in the Protheo project. My supervisors were Frédéric Blanqui and Claude Kirchner.

Enseignement

• 2009-2010 : Cours Logique de la programmation (M2 IF).
• 2010-2011 : TDs et TPs du cours Programmation 1 de Daniel Hirschkoff (L3 IF).
• 2010-2011 : Je partage avec Alexandre Miquel le cours Interprétations calculatoires des preuves (M2 IF).
• 2011-2012 : Cours Preuves (M1 IF).
• 2012-2013 : Cours Preuves sur ordinateur (M1 IF).
• 2013-2014 & 2014-2015 : Cours Computer Assisted Proofs (M1 IF).
• 2013-2014 & 2014-2015 : Cours CR03 (M2 IF) Recognizability and Model-Checking, from Automata to Lambda-Calculus.
• 2016-2017 : Cours CR05 Monadic Second Order Logic, Automata, Expressivity and Decidability (with Matteo Mio).
• 2018-2019 & 2019-2020 : Cours Advanced Topics in Semantics of Programming Languages (with Pierre Clairambault).
• 2020-2021 & 2021-2022 : Cours Logical Foundations of Programming Languages (with Olivier Laurent).
• 2020-2021 & 2021-2022 & 2022-2023 : Cours Proofs and Programs (M1 IF).
• 2015-2017 & 2018-2025 : Cours Semantics and Verification (M1 IF).

Informatique (CPES 2A Parcours Sciences)

• Page web du cours.

(Never Finished) Course Notes

• For the M1 course Proofs and Programs [pdf].
• For the M1 course Semantics and Verification [pdf].

Students

• Valentin Blot (Game Semantics and Classical Realizability).
• Cécilia Pradic (Proof Theoretical Approaches to MSO), co-advised with Henryk Michalewski.

Papers

Scott Domains

• Infinitary Refinement Types for Temporal Properties in Scott Domains.
  With Alexandre Kejikian.
  WoLLIC'25. arXiv.
• Liveness Properties in Geometric Logic for Domain-Theoretic Streams.
  With Solal Stern.
  JFLA'24. Full version [pdf] arXiv.
• On the Representation of Stream Functions in Denotational Domains.
  [pdf] (18 pages).

Arboreal Categories

• Finitely accessible arboreal adjunctions and Hintikka formulae.
  With Luca Reggio.
  arXiv.

Modal Logic and the Topos of Trees

• Temporal Refinements for Guarded Recursive Types.
  With Guilhem Jaber.
  ESOP'21. Full version [pdf].
• Modal Logic of Transition Systems in the Topos of Trees.
  With Guilhem Jaber.
  Full version [pdf].

Game Semantics and Tree Automata

• A Dialectica-Like Interpretation of a Linear MSO on Infinite Words.
  With Cécilia Pradic.
  FoSSaCS'19 [pdf].
• LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic.
  With Cécilia Pradic.
  LICS'18 [pdf].
• A Curry-Howard Approach to Church's Synthesis.
  With Cécilia Pradic.
  FSCD'17 [pdf].
  Long version LMCS, 15(4) (2019) [pdf].
• Monoidal Closed Categories of Tree Automata.
  MSCS, 30(1):62-117 (2020).
  Long version [pdf], slightly shortened version [pdf], and version with full proofs [pdf].
• Fibrations of Tree Automata.
  TLCA'15.
  Short version [pdf]. Full version [pdf].

Monadic Second-Order Logic

• A Complete Axiomatization of MSO on Infinite Trees.
  With Anupam Das. LICS'15.
  WARNING: There is an error in the uniform positional strategy argument in this paper.
  A weaker result is proved in:
  A Functional (Monadic) Second-Order Theory of Infinite Trees.
  With Anupam Das.
  LMCS, 16(4). Version with full proofs [pdf] (99 pages).
• Forcing MSO on Infinite Words in Weak MSO.
  LICS'13 [pdf] (15 pages).
• A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Infinite Words.
  IFIP-TCS'12 [pdf] (15 pages).
  Full version [pdf] (35 pages).

Realizability

• On Bar Recursion and Choice in a Classical Setting.
  With Valentin Blot.
  APLAS 2013. Full version [pdf].

Reducibility

• On the Values of Reducibility Candidates.
  TLCA'09 [dvi] [ps.gz] [pdf] (15 pages).
  Full version [dvi] [ps.gz] [pdf] (24 pages).
• Toward a General Rewriting-Based Framework for Reducibility.
  [pdf] (2008, 59 pages).
• Stability by Union of Reducibility Candidates for Orthogonal Constructor Rewriting.
  Invited paper for the special session "Higher-type recursion and applications" of CiE 2008.
  Full version [dvi] [ps.gz] [pdf] (14 pages).
• Strong Normalization as Safe Interaction.
  LiCS 2007. Full version [dvi] [ps.gz] [pdf] (14 pages).
• On the Stability by Union of Reducibility Candidates.
  FoSSaCS 2007 (a member conference of ETAPS 2007).
  Full version [dvi] [ps.gz] [pdf] (16 pages).

Termination

• A Tutorial on Type-Based Termination.
  With Gilles Barthe and Benjamin Grégoire.
  Book chapter LERNET 2008 Summer School, Springer LNCS Tutorial Series.
  Draft [dvi] [ps.gz] [pdf] (55 pages).
• Type-Based Termination with Sized Products.
  With Gilles Barthe and Benjamin Grégoire.
  CSL 2008. Full version [dvi] [ps.gz] [pdf] (39 pages).
• Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems.
  With Frédéric Blanqui.
  LPAR 2006 [dvi] [ps.gz] [pdf] (15 pages).

Confluence

• On the Confluence of λ-Calculus with Conditional Rewriting.
  With Frédéric Blanqui and Claude Kirchner.
  Journal version, Theoretical Computer Science 411 (2010) 3301-3327.
  Draft [dvi] [ps.gz] [pdf] (2009, 43 pages).
• On the Confluence of λ-Calculus with Conditional Rewriting.
  With Frédéric Blanqui and Claude Kirchner.
  FoSSaCS 2006 (a member conference of ETAPS 2006).
  Full version [dvi] [ps.gz] [pdf] (23 pages).

Phd Thesis

• Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage.
  In French (308 pages).

Contacts

• Email: colin.riba@ens-lyon.fr
• Postal address:
  LIP - École Normale Supérieure de Lyon
  46, allée d'Italie
  69007 Lyon
  France
  
• [Webmail] [Old Webmail] (for personnal use)