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-2016 & 2016-2017 & 2018-2019 & 2019-2020 & 2020-2021 & 2021-2022 & 2022-2023 : 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
- Internship proposal (Refinement Types for Liveness Properties in Denotational Semantics) [pdf].
- Valentin Blot (Game Semantics and Classical Realizability).
- Cécilia Pradic (Proof Theoretical Approaches to MSO), co-advised with Henryk Michalewski.
Papers
Scott Domains
-
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
Defended Friday, December 14th 2007 in Nancy.
-
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)
