I am a lecturer at the School of Computer Science of the University of Nottingham; I work in the Functional Programming Lab. My research interests are: type theory (with specific focus on corecursive structures), mathematical logic, proof assistants, (dependently typed) functional programming.
I received my laurea in matematica from the University of Padova and my PhD from the University of Nijmegen. I worked as a researcher at INRIA Sophia Antipolis, the University of Ottawa and the Radboud University Nijmegen.
Events
The
Midlands Graduate School in the Foundations of Computing Science.
Teaching
Mathematics for Computer Scientists (G51MCS)
Advanced Data Structures (G64ADS)
Dependently Typed Programming (G54DTP)
Ideas for Student Projects
Work in Progress
I'm working on Wander Types: a new data structure that unifies induction, coinduction and recursion.
Here is a draft article explaining them:
Wander Types: A Formalization of Coinduction-Recursion
I recently gave two talks about them:
This research is part of the project
Programming and Reasoning on Infinite Data Structures, supported by
EPSRC grant EP/I038713/1.
Publications
-
Coalgebras in functional programming and type theory
-
Theoretical Computer Science, in press
(bibtex entry).
-
Bisimulations Generated from Corecursive Equations
-
Electr. Notes Theor. Comput. Sci., 265: 245-258, 2010
(bibtex entry).
-
Corecursive Algebras: A Study of General Structured Corecursion
-
Coauthors: Tarmo Uustalu and Varmo Vene.
Formal Methods: Foundations and Applications, SBMF 2009, pages 84-100 (bibtex entry).
-
Higher-order abstract syntax in type theory
-
Coauthor: Amy Felty.
Logic Colloquium 2006, LNL 32, pages 65-90 (bibtex entry).
-
A Type of Partial Recursive Functions
-
Coauthor: Ana Bove.
TPHOLS 2008, pages 102-117 (bibtex entry).
-
Common Knowledge as a Coinductive Modality
-
Reflections on Type Theory, Lambda Calculus, and the Mind. Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday, December 2007, pages 51-61 (bibtex entry).
-
Computation by Prophecy
-
Coauthor: Ana Bove.
TLCA 2007, pages 70-83 (bibtex entry).
-
Formal Correctness of Conflict Detection for Firewalls
-
Coauthors: Bernard Stepien, Amy Felty, and Stan Matwin.
ACM Workshop on Formal Methods in Security Engineering, November 2007, pages 22-30 (bibtex entry).
-
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
-
Coauthor: Amy Felty.
TYPES 2006, LNCS 4502, pages 63-77 (bibtex entry).
-
Recursive Coalgebras from Comonads
(long version)
-
Coauthors: Tarmo Uustalu and Varmo Vene.
Information and Computation, volume 204, issue 4 (2006), pages 437-468 (bibtex entry).
-
Modelling general recursion in type theory
-
Coauthor: Ana Bove.
Mathematical Structures in Computer Science, Vol. 15, Iss. 4 (2005), pages 671-708
(bibtex entry).
-
General Recursion via Coinductive Types
(PostScript format)
-
Logical Methods in Computer Science, Vol. 1, Iss. 2 (2005), pages 1-28
(bibtex entry).
Coq formalization (requires vectors).
-
Recursive Functions with Higher Order Domains
-
Coauthor: Ana Bove.
In TLCA 2005, LNCS 3461, pages 116-130.
(bibtex entry).
-
Privacy in Data Mining Using Formal Methods
-
Coauthors: Stan Matwin, Amy Felty, and Istvan Hernádvölgyi.
In TLCA 2005, LNCS 3461, pages 278-292
(bibtex entry).
-
Recursive Coalgebras from Comonads
(short version)
-
Coauthors: Tarmo Uustalu and Varmo Vene.
Electronic Notes in Theoretical Computer Science,
Volume 106, Proceedings of CMCS 2004, pages 43-61
(bibtex entry).
- Setoids in type theory
-
Coauthors: Gilles Barthe and Olivier Pons.
In Journal of Functional Programming, 13(2), pages 261-293, 2003
(bibtex entry).
- Abstraction and Computation
-
Also in PostScript format.
PhD Thesis. Supervisor: Henk Barendregt. Defended on April 23, 2002. University of Nijmegen, The Netherlands.
- Type-theoretic functional sematics
-
Coauthors: Yves Bertot and Kuntal Das Barman.
In TPHOLs 2002, LNCS 2410, pages 83-97
(bibtex entry).
- Nested General Recursion and Partiality in Type Theory
-
Coauthor: Ana Bove.
In TPHOLs 2001, LNCS 2152, pages 121-135
(bibtex entry).
- Certifying the Fast Fourier Transform with Coq
-
In TPHOLs 2001, LNCS 2152, pages 154-168
(bibtex entry).
- The logic and mathematics of occasion sentences
-
Coauthors: Pieter A. M. Seuren and Herman Geuvers.
In Linguistics and Philosophy, 24(5), 2001
(bibtex entry).
- Recursive Families of Inductive Types
-
Also in PostScript format.
In TPHOLs 2000, LNCS 1869, pages 73-89
(bibtex entry).
- Universal Algebra in Type Theory
-
In TPHOLs 1999, LNCS 1690, pages 131-148
(bibtex entry).
- A general method for proving the normalization theorem for first and second order typed λ-calculi
-
Coauthor: Silvio Valentini.
In Mathematical Structures in Computer Science, volume 9, issue 6, pages 719-739, 1999
(bibtex entry).
