School of Computer Science
University of Nottingham
Jubilee Campus,
Wollaton Road
Nottingham NG8 1BB,
UK
office: B83
T: +44(0) 115 8232342
F: +44(0) 115 9514254
E: venanzio@duplavis.com
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.)
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 an 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
 Category Theory at MGS 2016
 The Category of Graphs
 Definition of Category, concrete categories
 Initial and Terminal Objects, duality, homsets
 Isomorphisms, monos, epis, products, sums
 Functors and Natural Transformations
 Constructions on Categories: Cat, slice categories, presheaves
 Exponentials, cartesian closed categories
 The Yoneda Lemma
 Adjunctions, (co)products, exponentials, and quantifiers as adjoints
 Advanced Functional Programming (G52AFP)
 Machines and their Languages (G52MAL)
 Mathematics for Computer Scientists (G51MCS)
 Advanced Data Structures (G64ADS)
 Dependently Typed Programming (G54DTP)
PhD Students
 Colm Baston (Epistemic Logic in Dependently Type Theory with Coinduction)
 Paolo Capriotti (Models of Type Theory with Strict Equality)
 Christian Sattler (On the Complexities of Polymorphic Stream Equation Systems, Isomorphism of Finitary Inductive Types, and Higher Homotopies in Univalent Universes)
 Florent Balestrieri (The Productivity of Polymorphic Stream Equations and the Composition of Circular Traversal)
Draft Papers
Publications

The Continuity of Monadic Stream Functions

Coauthor: Jonathan Fowler
Proceeding of LICS 2017, Reykjavik 2017
(slides from the talk)
(bibtex entry)

Contractive Functions on Infinite Data Structures

Coauthors: Graham Hutton and Mauro Jaskelioff
Prooceedings of IFL 2016, Leuven, Belgium

A Coalgebraic View of Bar Recursion and Bar Induction

Coauthor: Tarmo Uustalu.
Foundations of Software Science and Computation Structures (FOSSACS 2016), LNCS 9634, pages 91106
(bibtex entry).

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 coinductionrecursion

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: 245258, 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 84100 (bibtex entry).

Higherorder abstract syntax in type theory

Coauthor: Amy Felty.
Logic Colloquium 2006, LNL 32, pages 6590 (bibtex entry).

A Type of Partial Recursive Functions

Coauthor: Ana Bove.
TPHOLS 2008, pages 102117 (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 5161 (bibtex entry).

Computation by Prophecy

Coauthor: Ana Bove.
TLCA 2007, pages 7083 (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 2230 (bibtex entry).

Combining de Bruijn Indices and HigherOrder Abstract Syntax in Coq

Coauthor: Amy Felty.
TYPES 2006, LNCS 4502, pages 6377 (bibtex entry).

Recursive Coalgebras from Comonads
(long version)

Coauthors: Tarmo Uustalu and Varmo Vene.
Information and Computation, volume 204, issue 4 (2006), pages 437468 (bibtex entry).

Modelling general recursion in type theory

Coauthor: Ana Bove.
Mathematical Structures in Computer Science, Vol. 15, Iss. 4 (2005), pages 671708
(bibtex entry).

General Recursion via Coinductive Types
(PostScript format)

Logical Methods in Computer Science, Vol. 1, Iss. 2 (2005), pages 128
(bibtex entry).
Coq formalization (requires vectors).

Recursive Functions with Higher Order Domains

Coauthor: Ana Bove.
In TLCA 2005, LNCS 3461, pages 116130.
(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 278292
(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 4361
(bibtex entry).
 Setoids in type theory

Coauthors: Gilles Barthe and Olivier Pons.
In Journal of Functional Programming, 13(2), pages 261293, 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.
 Typetheoretic functional sematics

Coauthors: Yves Bertot and Kuntal Das Barman.
In TPHOLs 2002, LNCS 2410, pages 8397
(bibtex entry).
 Nested General Recursion and Partiality in Type Theory

Coauthor: Ana Bove.
In TPHOLs 2001, LNCS 2152, pages 121135
(bibtex entry).
 Certifying the Fast Fourier Transform with Coq

In TPHOLs 2001, LNCS 2152, pages 154168
(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 7389
(bibtex entry).
 Universal Algebra in Type Theory

In TPHOLs 1999, LNCS 1690, pages 131148
(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 719739, 1999
(bibtex entry).