Introduction to Constructive Set Theory",
talk given to the Leeds Maloa training workshop, 30th June, 2011.
On Voevodsky's Univalence Axiom",
talk given at the Third European Set Theory Conference,
6th July, 2011, Edinburgh.
Generalised Type Setups for Dependently Sorted Logic",
talk given at TACL 2011, 26th July, Marseille.
What is a set?",
talk given to the Leeds Logic seminar, 24th November, 2010.
Some Weak Axiom Systems for CST",
talk given at the Kanazawa workshop on "Constructive
Aspects of Logic and Mathematics", March 8-12, 2010.
The Type Theoretic Concept of Set",
talk given at the meeting "Set Theory, Classical and Constructive",
Amsterdam, May 6-7, 2010.
Rudimentary Constructive Set Theory",
talk given at the meeting "Set Theory, Model Theory, Generalized
Quantifiers and Foundations of Mathematics: Jouko birthday conference!
Meeting in Honor of Jouko Vaananen Sixtieth Birthday",
Helsinki, 16-18 September 2010 .
Explicit Set Existence",
talk given at the meeting "Symposium on Proof Theory
and Constructivism", Leeds, July, 2009.
Predicate Logic over a Type Setup",
talk given at the meeting "Philosophy and Foundations of Mathematics:
Epistemological and Ontological Aspects",
a conference dedicated to Per Martin-Lof
on the occasion of his retirement, Uppsala, May 2009.
Identity Types and Type Setups",
seminars given in Uppsala and Gothenberg, February, 2009
Core Extensional Mathematics and Local Constructive Set Theory
", talk given in Padua in October, 2008, at the meeting
"Advances in Constructive Topology and Logical Foundations", in honour of
the 60th birthday of Giovanni Sambin.
Constructive Set Theory",
Mathlogaps Summer School lecture course, Manchester, July 2008
Local Constructive Set Theory",
talk given at Oberwolfach, April, 2008.
Predicate Logic over a Type Setup
",, talk given at Russell'08, Swansea, March, 2008.
On avoiding dependent choices in formal topology",
3WFTop talk, Padua, May 2007.
For printing use " 20 pages",
Are There Enough Injective Sets?",
by Peter Aczel, Benno van den Berg, Johan Granstroem,
Peter Schuster. To appear in Studia Logica, 2012?
Generalised type setups for dependently sorted
Extended abstract for a talk given at TACL 2011.
Local Constructive Set Theory and Inductive
, in "Foundational Theories of Classical and
Constructive Mathematics", (edited by Giovanni Sommaruga),
The University of Western Ontario Series in Philosophy of
Science, Springer, 2011.
Equalisers of frames in constructive set theory",
in "Logic, Mathematics, Philosophy, Vintage Enthusiasms (Essays
in honour of J. Bell)",(edited by David DeVidi, Michael Hallett
and Peter Clark), The University of Western Ontario Series in
Philosophy of Science, Volume 75, Part 3, Springer, 2011.
On the T1 Axiom and Other Separation Properties in Constructive
Point-free and Point-set Topology,
, by Peter Aczel and Giovanni Curi, published in APAL, 161
(2010) pp. 560-569.
- "A constructive version of the Lusin
, in the book
`Logicism, Intuitionism and Formalism--What has become of them?',
(LindstrÃ¶m, S., Palmgren, E., Segerberg, K. and Stoltenberg, V. eds.),
Synthese Library, Springer, pp. 129-151, 2009.
- "The Relation Reflection Scheme",
, in the special issue of the Mathematical
Logic Quarterly, edited by Julia Zappe, Josef Berger, Peter Schuster
and Dirk Pattinson (guest editors), Vol 54, No.1, pp. 5-11, 2008.
Binary Refinement Implies Discrete Exponentiation",
, by Peter Aczel, Laura Crosilla, Hajime Ishihara, Erik
Palmgren and Peter Schuster, in Studia Logica 84 (2006) 361-368.
Aspects of General Topology in Constructive Set Theory",
in the proceedings of the second workshop of Formal
Topology in a special issue of the Annals of Pure and Applied
Logic, 137 (2006) 3-29.
The Generalised Type_theoretic Interpretation of
Constructive Set Theory},
by Nicola Gambino and Peter Aczel,
in the Journal of Symbolic Logic, Volume 71, Number 1,
March (2006), 67-103.
Separation properties in Constructive Topology",
by Peter Aczel and Chris Fox, in `From Sets and Types to Topology and
Analysis'. Towards Practicable Foundations of Constructive Mathematics
(L. Crosilla, P. Schuster, eds.), Oxford Logic Guides,
Oxford University Press, pp 176-192, October 2005.
Some Older Published Papers
"Infinite trees and completely iterative theories: a coalgebraic
by P. Aczel, J.Adamek, S.Milius and J. Velebil, to appear
in Theoretical Computer Science (2003)
"Algebras and Coalgebras", in "Algebraic and Coalgebraic
methods in the Mathematics of Program Construction", edited by
R. Backhouse, R. Crole and Jeremy Gibbons, the
proceedings of an April 2000 International Summer School and
Workshop, LNCS 2297 (2002)
- "Collection Principles in Dependent Type Theory",
by P. Aczel and N. Gambino, in "Types for Proofs and Programs",
edited by P.Callaghan, Z. Luo, J. Mckinna and R. Pollack, the
proceedings of the 2000 workshop, LNCS 2277 (2002)
preliminary version in
"gzipped ps file",,
Frame-valued Semantics for Constructive Set Theory",,
by P. Aczel and N. Gambino, Mittag-Leffler Technical Report No.39, 2000/2001
Notes on Constructive Set Theory",,
written with Michael Rathjen, Mittag-Leffler Technical Report No.40,
2000/2001. [This is an improved and extended version of the draft 1997
"Notes on Constructive Set Theory".]
A Coalgebraic View of Infinite Trees and Iteration",,
written with J. Adamek and J. Velebil, Electronic Notes in
Theoretical Computer Science 44.1 (2001)
- "The Russell-Prawitz Modality",
Mathematical Structures in Computer Science (2001), vol
[Preliminary version in
Technical Report Series, Department of
Computer Science, University of Manchester,
- "On relating type theories and set
in "Types for Proofs and Programs", edited by
Altenkirch, Naraschewski and Reus, Proceedings of Types '98,
SLNCS 1657 (1999).
- "Notes on the simply typed
In the Proceedings of the 1997 "Computational Logic" Advanced Study
Institute International Summer School at Marktoberdorf, (1999).
- "Lectures on Semantics
: The initial algebra and final coalgebra perspectives"
Four lectures given at the 1995 "Logic of Computation" Advanced Study
Institute International Summer School at Marktoberdorf, in ``Logic of
Computation'', edited by H. Schwichtenberg, Springer (1997).
- "Generalised Set Theory",
in Logic, Language and Computation, Jerry Seligman and Dag Westerstahl,
eds, CSLI Lecture Notes No. 58, Stanford University, (1996).
"Final Universes of Processes",
in the proceedings of the 9th International
Conference on Mathematical Foundations of Programming Semantics, edited by
S.Brookes, M.Main, A.Melton, M.Mislove and D.Schmidt, SLNCS 802, pp 1-28,
- "Schematic Consequence",
in "What is a Logical System", edited by Dov Gabbay, OUP, (1994).
- "Term Declaration Logic",
in Proceedings of the 6th annual IEEE Symposium on Logic in CS, (1991).
Some Older Unpublished Reports and Slides
- "Notes on Constructive Set Theory",
This is the previous 1997 version of
"Notes on Constructive Set Theory",
- "Constructive Type Theory",
Six lectures given at the 1997 "Computational Logic" Advanced Study
Institute International Summer School at Marktoberdorf, July/August 1997.
- "A Semantic Universe for the study of
- "A notion of class for theory development in Algebra (in a
predicative type theory).
Partially in collaboration with
Gilles Barthe. Slides for a talk in Bastad, Sweden in June, 1994.
Simple overloading for type theories, June 23, 1994
A notion of class for Type Theory.
DRAFT with Gilles Barthe, Manchester, August 16, 1993",
- "A direct constructive treatment of the
Fundamental Theorem of Galois Theory, DRAFT",
- "Galois: A Theory Development Project",
Report for the 1993 Turin meeting on the Representation of
Mathematics in Logical Frameworks.
Lecture Series at Padua University, Spring 1998
A 1980 unpublished paper
An old, but influental 1978 unpublished paper
Peter Aczel's home page
Last updated: October 29th, 2014