Recent Slides

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

• " Equalisers of frames in constructive set theory", to appear, 2009/2010.

• " Local Constructive Set Theory and Inductive Definitions, , to appear.

• " On the T1 Axiom and Other Separation Properties in Constructive Point-free and Point-set Topology, , by Peter Aczel and Giovanni Curi, to appear in APAL, 2009.

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

• "Galois: A Theory Development Project", Report for the 1993 Turin meeting on the Representation of Mathematics in Logical Frameworks.

• "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 direct constructive treatment of the Fundamental Theorem of Galois Theory, DRAFT",
  

Lecture Series at Padua University, Spring 1998

• Notes for the lectures on Constructive Set Theory

An old, but influental unpublished paper

• A General Church-Rosser Theorem

My logic Ph.D. research pages

• Formalisation in Theory and Practice

• Variants of Classical Set Theory and Their Applications

Return to Peter Aczel's home page

Last updated: January 22nd, 2007