Recent Slides

• " 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",

Recent papers

• " 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 logic", Extended abstract for a talk given at TACL 2011.

• " Local Constructive Set Theory and Inductive Definitions, , 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 Separation Theorem", , 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 view" 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 11,pp. 541-554.
  [Preliminary version in Technical Report Series, Department of Computer Science, University of Manchester, UMCS-00-12-1 .]
• "On relating type theories and set theories", in "Types for Proofs and Programs", edited by Altenkirch, Naraschewski and Reus, Proceedings of Types '98, SLNCS 1657 (1999).

• "Notes on the simply typed lambda calculus" 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, (1994).

• "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 Fairness",
  

• "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

• Notes for the lectures on Constructive Set Theory

A 1980 unpublished paper

• A Note on Interpreting Intuitionistic Higher Order Logic

An old, but influental 1978 unpublished paper

• A General Church-Rosser Theorem

Return to Peter Aczel's home page

Last updated: October 29th, 2014