Contents
|
Latest updates
3/5/2012
|
The paper Inductive types in homotopy type theory,
written
with
S.
Awodey
and
K.
Sojakova,
has
been accepted for publication in the proceedings of LICS 2012.
The paper is available on ArXiv
and the related Coq code on Github.
|
| 22/3/2012 |
Steve Awodey, Erik
Palmgren and I are co-editing a special issue of Mathematical
Structures in
Computer Science, entitled "From Type Theory and Homotopy Theory to
Univalent Foundations". For more information, see the call for
papers. |
| 7/2/2012 |
The workshop Higher-dimensional algebra,
categories and types will be held in Ljubljana (Slovenia) on June
20th, 2012, immediately after the Fourth
Workshop
on
Formal
Topology |
Research
interests
- Mathematical Logic (proof theory, constructive set theory,
type
theory, categorical logic)
- Category Theory (2-categories, homotopical algebra,
polynomial
functors)
- Theoretical Computer Science (computer-assisted
proof-checking)
Publications
- Inductive types in
Homotopy Type Theory, written with S. Awodey and K. Sojakova
Proceedings of the
Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science
(LICS 2012). Forthcoming.
- Double adjunctions
and
free
monads, written with T. M. Fiore and J. Kock
Cahiers de Topologie et
Géométrie Differentielles Catégoriques, Forthcoming.
- Monads in double
categories, written with T. M. Fiore and J. Kock
Journal
of Pure and Applied Algebra 215 (6) 2011, pp. 1174-1197.
- Weighted
limits
in
simplicial
homotopy
theory
Journal
of
Pure
and
Applied
Algebra 214 (7) 2010, pp. 1193-1199.
- Lawvere-Tierney
sheaves
in
Algebraic
Set
Theory, written with S. Awodey, P. L. Lumsdaine and M. A. Warren
Journal of Symbolic
Logic
73
(3) 2009, pp. 861-890.
- The
identity type weak
factorisation system, with R. Garner
Theoretical
Computer Science
409
(1) 2008, pp. 94-109.
- The
associated
sheaf
functor
theorem
in
Algebraic
Set
Theory
Annals of Pure and
Applied Logic 56
(1) 2008, pp. 68-77.
- Homotopy
limits
for
2-categories
Mathematical
Proceedings of the Cambridge Philosophical Society
145 (1) 2008, pp. 43-63.
- The
cartesian
closed
bicategory
of
generalised
species
of
structures, written with M. Fiore, M. Hyland and G. Wynskel
Journal of the London
Mathematical
Society
77 (2) 2008, pp.
203-220.
- Spatiality
for
formal
topologies, written with P. Schuster
Mathematical
Structures in Computer Science 17 (1) 2007, pp.
65-80.
- Heyting-valued
interpretations
for
constructive
set
theory
Annals
of Pure and
Applied Logic 137 (1-3) 2006, pp. 164-188.
- The
generalised
type-theoretic
interpretation
of
constructive
set
theory, written with P. Aczel
Journal of Symbolic
Logic 71
(1) 2006, pp. 67-103.
- Presheaf
models
for
Constructive
Set
Theories
In L. Crosilla and P.
Schuster (editors), From Sets and Types to Topology and Analysis,
Oxford
University
Press,
2005,
pp.
62-77.
- Wellfounded
Trees
and
Dependent
Polynomial
Functors, written with M. Hyland
In S. Berardi and M. Coppo
and F. Damiani (editors), Types for proofs and programs,
Lecture Notes in Computer Science 3085, Springer (2004), pp. 210-225.
- Collection
Principles
in
Dependent
Type
Theory, written with P. Aczel
In Z. Luo and J. McKinna and
R. Pollack (editors), Types for proofs and programs, Lecture
Notes in Computer Science 2277, Springer (2002), pp. 1-23.
Preprints
- Polynomial
functors
and
polynomial
monads, written with J. Kock, ArXiv:0906:4931, 2010.
Survey papers
- On
the
coherence conditions for pseudo-distributive laws, arXiv:0907:1359,
2009.
Slides of
talks
- Constructive
Mathematics
in
Constructive
Set
Theory, Second MALOA Training
Workshop, Leeds, June 30th, 2011.
- Homotopy-theoretic
aspects
of
Martin-Löf
type
theory, Logic Colloquium 2010, Paris, July
30th,
2010.
- Polynomial
Functors
and
Polynomial
Monads, Leeds
Symposium
in Proof Theory
and Constructivism, July 13th 2009.
- Lectures
on
Dependent
Type
Theories, Midlands
Graduate
School 2009,
Leicester, March 30th - April 3rd, 2009.
Editorial duties
Teaching
Contact
details
| Dipartimento di Matematica
e Applicazioni |
Email: ngambino AT math
DOT unipa DOT it
|
| Università degli
Studi di Palermo |
Phone: +39 091 238 91 048
|
| via Archirafi 34 |
Fax: +39 091 238 91 024
|
| 90123 Palermo |
|
| ITALY |
|
|