Venanzio Capretta
Portrait 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 assistant professor 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

Past teaching

PhD Students

Publications

Reflection in the Chomsky hierarchy
Coauthors: Henk Barendregt and Dexter Kozen.
Journal of Automata, Languages and Combinatorics, 18(1), 2013 (bibtex entry).
Wander types : A formalization of coinduction-recursion
Progress in Informatics, 2013 (bibtex entry).
Slides from two talks about Wander types:
Coalgebras in functional programming and type theory
Theoretical Computer Science, 412 (38), pg. 5006 - 5024, 2011 (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).