Venanzio Capretta

School of Computer Science
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB, UK
office: A07

T: +44(0) 115 8232342
F: +44(0) 115 9514254
E: venanzio@duplavis.com

Bookcover of Reflections

REFLECTIONS on Type Theory, Lambda Calculus, and the Mind

Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday

Erik Barendsen, Herman Geuvers, Venanzio Capretta, Milad Niqui (Eds.)

Bookcover of Abstraction and Computation

Abstraction and Computation
Type Theory, Algebraic Structures, and Recursive Functions

My PhD Thesis.
Supervisor: Henk Barendregt.
Defended on April 23, 2002. University of Nijmegen, The Netherlands.

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.

Teaching

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
Extended and revised on 9 May 2012.

Last year I 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).