Research:	Proof Theory, esp. of Martin-Löf Type Theory, Programming with Dependent Types, esp. Interaction and Induction-Recursion. More on A. Setzer's Research Chair person of the Swansea subsite of the TYPES project EPSRC Grant GR/S30450/01: Extension of Dependent Type Theory - Induction, Interaction, Universes
Talks given:	Slides of talks given
Conference Organisation/ Programme Committee
	British Logic Colloquium 2009 CSL 2009 Russell'08 - Proof theory meets Type Theory PCC 2007 Computability in Europe, CiE 2006 Constructive Logic in Software Engineering, CLASE 2005 (ETAPS)
Modules:	CS_236: Language and Compuation CS_313: High Integrity Systems CS_M00: Research Methodology (Coordination) CS_M13: Critical Systems
Modules taught in previous years:	CS_113: From Languages to Hardware CS_199: Computers Unplugged (Chapter on Languages) CS_226: Computability Theory CS_336: Interactive Theorem Proving CS_M33: Computer Systems: Processors, Memory, Data CS_M36: Functional Programming and Interactive Theorem Proving (Part II) CS_M46: Interactive Theorem Proving
Administrative duties:
	Liason officer for Mathematics. Member of the Examination team (Examination Results)
Other:
	Informations for tutorial and project students(Including some new items) Software Maintainer of links to logic-servers world wide My current timetable can be found here Further information on A. Setzer Links
Contact
Tel. :	International: +44 1792 513368 National: 01792 513368
Fax:	International: +44 1792 295708 National: (01792) 295708
Email:
Address:	Dr. Anton Setzer, Dept. of Computer Science, Swansea University, Singleton Park, Swansea, SA2 8PP, UK
Visiting Address:	Faraday Building, Computer Science Department, 2nd floor, room 211
More information:	Further information on A. Setzer (research, other courses, links) can be found here
	Back to academic staff at the Dep. of Computer Science

Publications of Anton Setzer

(Reportform, theses etc see below)

• Thorsten Altenkirch, Peter Morris, Fredrik Forsberg and Anton Setzer: A categorical semantics for inductive-inductive definitions.
  • To appear in Corradini, Andrea and Klin, Bartek, CALCO 2011
  • BibTeX
  • Draft Version
    • Pdf
• Fredrik Forsberg, Anton Setzer: Inductive-inductive Definitions.
  • In Anuj Dawar and Helmut Veith: CSL 2010. Proceedings. Lecture Notes in Computer Science, 454 - 468
  • BibTeX
  • Draft Version
    • pdf
    • ps
    • dvi
• Reinhard Kahle, Anton Setzer: An extended predicative definition of the Mahlo universe.
  • In: Ralf Schindler (Eds): Ways of ProofTheory. Ontos Series in Mathematical Logic, Ontos Verlag, Frankfurt (Main), Germany, 2010, pp. 315 - 340.
  • Webpage with articles of the Festschrift
  • BibTeX
  • Draft Version
    • pdf
    • ps
    • dvi
• Karim Kanso, Faron Moller, Anton Setzer: Automated Verification of Signalling Principles in Railway Interlocking Systems
  • Electronic Notes in Theoretical Computer Science 250 (2009) 19 - 31. DOI 10.1016/j.entcs.2009.08.015.
  • draft version (dvi)
  • draft version (pdf)
  • bibtex
• Anton Setzer: Proof Theory and Martin-Löf Type Theory
  • In M. v. Atten, P. Boldini, M. Bourdeau, G. Heinzmann (Eds): One Hundred Years of Intuitionism (1907 -- 2007). Birkhäuser, 2008, pp. 257 -- 279. ISBN: 978-3764386528.
  • Bibtex-entry
  • Draft version:
    • dvi
    • ps
    • pdf
• A. Setzer: Universes in Type Theory I -- Inacccessibles and Mahlo
  • In: A. Andretta, K. Kearnes and D. Zambella: Logic Colloquium 2004. Association of Symbolic Logic, Lecture Notes in Logic, 29, Cambridge University Press, 2008, pp. 123 - 156. ISBN: 978-0521884242.
  • BibTeX-Entry.
  • Draft version:
    • dvi
    • postscript.
    • pdf-file.
• Rose H. Abdul Rauf, Ulrich Berger, Anton Setzer: A provably correct translation of the lambda-calculus into a mathematical model of C++
  • Jour. Theory of Computing Systems, Vol. 43, Issue 3, December 2008, pp. 298 - 321. DOI: 10.1007/s00224-007-9062-1.
  • BibTeX
  • Draft version:
    • dvi file
    • Postscript
    • Pdf version
• Rose H. Abdul Rauf, Ulrich Berger, Anton Setzer: Functional Concepts in C++.
  • In: Henrik Nilsson (Ed.): Trends in Functional Programming. Volume 7, Series Trends in Functional Programming, Intellect, Intellect, Bristol and Chicago, 2007, pp. 163 -- 179.
  • BibTeX
  • Draft version:
    • dvi file
    • Postscript
    • Pdf version
• Will Harwood, Faron Moller, Anton Setzer: Weak Bisimulation Approximants
  • In: Zoltán Ésik (Ed): Computer Science Logic. 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006. Proceedings. Springer Lecture Notes in Computer Science 4207, 2006, pp. 365 - 379.
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Get article from Springer using DOI
  • Postscript
  • Pdf
  • BibTeX
• Anton Setzer: Object-oriented programming in dependent type theory
  • In: Henrik Nilsson (Ed.): Trends in Functional Programming. Volume 7, Series Trends in Functional Programming, Intellect, Intellect, Bristol and Chicago, 2007, pp. 91 -- 108.
  • BibTeX
  • Draft version:
    • dvi file
    • Postscript
    • Pdf version
• Anton Setzer: Partial recursive functions in dependent type theory
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • In: Arnold Beckmann, Ulrich Berger, Benedikt Löwe, John V. Tucker (Eds): Logical Approaches to Computational Barriers: Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006. Springer Lecture Notes in Computer Science, 3988, pp. 505 -- 515, 2006.
  • Published Version by Springer is available here
  • dvi
  • ps
  • pdf
  • Bibtex-entry
• P. Dybjer, A. Setzer: Indexed Induction-Recursion. Long version.
  • Journal of Logic and Algebraic Programming 66, 1 - 49, 2006.
  • BibTeX-Entry.
  • Published version via DOI
  • Draft version:
    • dvi.
    • postscript.
    • pdf-file.
• Markus Michelbrink, Anton Setzer: State-dependent IO monads in type theory
  • Electronic Notes in Theoretical Computer Science, 122 (2005) 127 -- 146.
  • Final Version available from Elsevier
  • BibTeX.
  • Draft version:
    • postscript.
    • pdf-file.
• Peter Hancock, Anton Setzer: Interactive programs and weakly final coalgebras in dependent type theory.
  • In: L. Crosilla and P. Schuster (Eds.): From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, Clarendon Press, Oxford, 2005, pp. 115 - 134.
  • BibTeX.
  • Draft version:
    • dvi (diagrams don't show well; use ps or pdf instead).
    • postscript.
    • pdf-file.
• A. Setzer: Proof Theory of Martin-Löf Type Theory -- An Overview.
  • Mathematiques et Sciences Humaines, 42 année, 165, 2004, p. 59--99.
  • BibTex
  • Draft version:
    • Postscript
    • Pdf
• P. Dybjer, (Göteborg) and A. Setzer: Induction-Recursion and initial algebras. Annals of pure and applied logic, 124 (2003), 1 -- 47.
  • Published version from elsevier (Requires that you have access to the electronic version of this journal).
  • BibTeX-entry
  • Draft version:
    • dvi Version (Diagrams look better in the postscript version).
    • postscript.
    • pdf-file
• A. Setzer: Java as a functional programming language.
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • In: Herman Geuvers, Freek Wiedijk (Eds.): Types for Proofs and Programs: International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002. Selected Papers. Springer Lecture Notes in Computer science 2646, 2003, pp. 279 - 298.
  • dvi
  • postscript
  • pdf-file
  • BibTeX Entry
• P. Dybjer, A. Setzer: Indexed Induction-Recursion (Diagrams look better in ps/pdf version).
  • In: R. Kahle, P. Schroeder-Heister, R. Stärk (Eds.): Proof Theory in Computer Science. LNCS 2183, pp. 93 -- 113, 2001
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • postscript.
  • pdf-file.
  • BibTeX-entry.
• Peter Hancock, Anton Setzer: Interactive programs in dependent type theory
  • In: P. Clote, H. Schwichtenberg: Computer Science Logic. 14th international workshop, CSL 2000. Springer Lecture Notes in Computer Science, Vol. 1862, pp. 317 - 331, 2000.
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • postscript.
  • pdf-file.
  • bibtex.
  • Preprint version: Interactive programs in dependent type theory. U.U.D.M. Report 2000:5, ISSN 1101-3591, Dept. of Mathematics, Uppsala University, February 2000. (postscript, pdf-file)
• A. Setzer: Extending Martin-Löf Type Theory by one Mahlo-Universe. Arch. Math. Log (2000), 39: 155 - 181.
  • BibTeX Entry.
  • Draft version:
    • dvi
    • postscript.
    • pdf-file.
• A. Setzer:Ordinal systems part 2: One inaccessible.
  • In: S. Buss, P. Hajek, P. Pudlak (Eds.): Logic Colloquium '98. ASL Lecture Notes in Logic 13, Peters Ltd, Natick, Massachusetts, 2000, pp. 426 - 448.
  • BibTeX-entry.
  • Draft version:
    • dvi
    • postscript.
    • pdf-file.
• P. Dybjer, (Göteborg) and A. Setzer A finite axiomatization of inductive-recursive definitions.
  • In: Girard, J.-Y. (Ed.): Typed Lambda Calculi and Applications. Proceedings of TLCA'99, L'Aquila, Italy, Springer Lecture Notes in Computer Science, Vol. 1581, pp. 129 - 146, 1999.
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • postscript.
  • pdf-file.
  • BibTeX-entry.
• G. Jäger, Reinhard Kahle, Anton Setzer, T. Strahm: The proof-theoretic analysis of transfinitely iterated fixed point theories.
  • In Journal of Symbolic Logic 64, 1: 53 - 67, 1999.
  • BibTeX
  • Published Version
  • Draft version:
    • pdf
• A. Setzer: Ordinal systems.
  • In B. Cooper and J. Truss (Eds.): Sets and Proofs, Cambridge University Press, Cambridge, pp. 301 - 331, 1999.
  • Bibtex-entry
  • Some mistakes have been detected. Here are the corrections:
    • Corrections
      • postscript
      • pdf-file
    • Corrected version of Ordinal Systems
      • postscript
      • pdf-file
      • Some people have problems with printing this file, therefore here is the Latex-source
• Peter Clote, Anton Setzer: On PHP, st-connectivity, and odd charged graphs
  • In: P. Beame, S. Buss (Eds.): Proof complexity and feasible arithemetics. DIMACS workshop April 21 - 24, 1996. American Mathematical Society, 1998, pp. 73 - 92.
  • Draft version:
    • pdf-file.
• A. Setzer: Well-ordering proofs for Martin-Löf Type Theory with W-type and one Universe. Annals of Pure and applied Logic, 92 (1998), 113 - 159.
  • Bibtex entry
  • Draft version:
    • dvi
    • postscript.
    • pdf-file.
  • Reviewed in Bulletin of Symbolic Logic, Vol. 6, Number 4, Dec 2000, pp. 478 - 479
• A. Setzer: An introduction to well-ordering proofs in Martin-Löf's type theory.
  • In: G. Sambin and J. Smith (Ed.): Twenty-five years of constructive type theory, Clarendon Press, Oxford, 1998, pp. 245 - 263.
  • Draft version:
    • Bibtex entry
    • dvi
    • postscript.
    • pdf-file.
• A. Setzer: Translating set theoretical proofs into type theoretical programs.
  • In: G. Gottlob, A. Leitsch, D. Mundici (Eds.): Computational Logic and Proof Theory. 5th Kurt Gödel Colloquium, KGC' 97. Springer Lecture Notes in Computer Science, 1289, 1997, pp. 278 - 289.
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Published Version by Springer is available here
  • postscript.
  • pdf-file.
• A. Setzer: Inductive definitions with decidable atomic formulas.
  • In: D. van Dalen, M. Bezem (Eds.): Computer Science Logic. 10th International workshop CSL '96. Springer Lecture Notes in Computer Science, 1258, 1997, pp. 414 - 431.
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Published Version by Springer is available here
  • postscript.
  • pdf-file.

Theses

• A. Setzer: Proof theoretical analysis of Martin-Löf Type Theory with W-type and one Universe.
  • PhD-thesis, 140 pp., 1993.
  • postscript.
  • pdf-file.
  • Bibtex-entry.
• A. Setzer: Ordinalzahlanalyse prädikativer Theorien unter Verwendung von Fundamentalfolgen. Master's Thesis, 116 pp., 1990.
  • postscript.
  • pdf-file.
  • Bibtex-entry.

Reports, Submissions, Electronic Proceedings

• Anton Setzer: Coalgebras as Types determined by their Elimination Rules
  • Submitted to: Peter Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm: Epistemology versus ontology: Essays on the foundations of mathematics in honour of Per Martin-Löf. Springer, 2011.
  • Submited version
    • dvi
    • ps
    • pdf
    • bib
• Karim Kanso, Anton Setzer: A light-weight integration of automated and interactive theorem proving.
  • Submitted to Math. Struct. in Comp. Science.
  • pdf-file
• Karim Kanso, Anton Setzer: Integrating Automated and Interactive Theorem Proving in Type Theory.
  • In: Jens Bendisposto, Michael Leuschel, Markus Roggenbach (Eds.): Proceedings of AVOCS 2010.
  • BibTeX
  • Pdf
• Anton Setzer: Universes in Type Theory Part II -- Autonomous Mahlo.
  • After revision accepted for publication in Journal of Symbolic Logic, 2010
  • BibTeX
  • Draft Version
    • pdf
    • ps
    • dvi
• Karim Kanso, Anton Setzer: Specifying Railway Interlocking Systems.
  • In: Liam O'Reilly and Markus Roggenbach: AVoCS'09 -- PreProceedings of the Ninth International Workshop on Automated Verification of Critical Systems. Swansea University, Wales, UK, Technical Report of Computer Science CSR-2-2009, 2009, pp 233 -- 236, http://www.cs.swan.ac.uk/avocs09/PreProceedings.pdfhttp://www.cs.swan.ac.uk/avocs09/PreProceedings.pdf.
  • dvi
  • pdf
  • BibTeX
• Karim Kanso, Faron Moller, Anton Setzer: Automated Verification of Safety Properties in Railway Interlocking Systems Defined with Ladder Logic
  • In: Muffy Calder and Alice Miller (Eds.): Proceedings of AVOCS'08. Eighth International Workshop on Automated Verification of Critical Systems. University of Glasgow, 30. Sept. -- 1 Oct 2008, 2008, pp. 77 -- 79.
  • dvi
  • ps
  • pdf
  • BibTeX
• Anton Setzer: A data type of partical recursive functions in Martin-Löf type theory
  • Submitted.
  • dvi
  • ps
  • pdf
  • Bibtex-entry
• Anton Setzer: Object-oriented programming in dependent type theory
  • In conference proceedings of TFP 2006, 2006.
  • dvi file
  • Postscript
  • Pdf version
  • BibTeX
• Rose H. Abdul Rauf, Ulrich Berger, Anton Setzer: Functional Concepts in C++
  • In conference proceedings of TFP 2006, 2006.
  • dvi file
  • Postscript
  • Pdf version
  • BibTeX
• Anton Setzer: Universes in Type Theory Part II -- Autonomous Mahlo and Pi_3-Reflection.
  • 32 pages, submitted, 2005.
  • dvi
  • postscript
  • pdf-file
  • BibTeX-Entry
• Peter Hancock, Anton Setzer: Guarded induction and weakly final coalgebras in dependent type theory (Extended Version)
  • 30 pages. In electronic proceedings of the workshop No. 04381 ``Dependently typed programming'', Dagstuhl, 2004, http://drops.dagstuhl.de/opus.
  • dvi (diagrams don't show well; use ps or pdf instead).
  • postscript.
  • pdf-file.
  • BibTeX.
• Peter Hancock, Anton Setzer: Specifying interactions with dependent types,
  Workshop on subtyping and dependent types in programming, Ponte de Lima, Portugal, 7 July 2000. 13 pages.
  • pdf-file
  • postscript
  • BibTeX-Entry
• Peter Hancock, Anton Setzer: The IO monad in dependent type theory
  ( Workshop on Dependent Types in Programming, Göteborg 27-28 March 1999)
  • Extended slides:
    • dvi,
    • postscript,
    • pdf-file,
    • BibTeX-Entry.
  • Normalizing version with state-dependend IO, type checked in Half
• P. Dybjer, (Göteborg) and Anton Setzer: Finite axiomatizations of inductive and inductive-recursive definitions.
  (Workshop on Generic Programming Marstrand, Sweden, 18 June 1998)
  • postscript.
  • pdf-file.
  • bibTeX-Entry.

Reviews

• Bulletin of Symboli Logic
  • Review of J. Roger Hindley, Basic simple type theory, Bull. Sym. Log., 64, 4: 1832 - 1833, 1999
• Zentralblatt MATH
  • Tupailo, Sergei: Finitary reductions for local predicativity. I: Recursively regular ordinals. In Buss, Samuel R. (ed.) et al., Logic colloquium '98. A K Peters, Lect. Notes Log. 13, 465-499 (2000). Zentralblatt MATH, 0949.03053
  • J. Avigad. Interpreting classical theories in constructive ones. J. Symb. Log. 65, No. 4, 1785-1812 (2000). Review No. 0981.03061.
  • A. Troelstra; H. Schwichtenberg: Basic proof theory. 2nd Ed. Cambridge University Press. 417 p., 2000. Review No. 0957.03053.
  • W. Buchholz: Explaining the Gentzen-Takeuti reduction steps: A second-order system. Arch. Math. Log. 40, No. 4, 255-272 (2001). Review No. Zbl 1007.03051.
  • S. Buss; P. Pudlak: On the computational content of intuitionistic propositional proofs. Ann. Pure Appl. Logic 109, No. 1-2, 255-272 (2001). Review No. Zbl 1009.03027.
  • T. Carlson: Elementary patterns of resemblance. Ann. Pure Appl. Logic 108, No. 1-3, 19-77 (2001). Review No. Zbl. 1009.03026.
  • C. Urban; G. Bierman: Strong normalisation of cut-elimination in classical logic. Fundam. Inform. 45, No. 1-2, 123-155 (2001). Review No. Zbl 0982.03032.
• Mathematical Reviews
  • P. Dybjer: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log. 65 (2000), no. 2, 525-549. Review No. 2001i:03025.
  • S. Feferman: Does reductive proof theory have a viable rationale? Erkenntnis 53, 63-96 (2000). Review No. 2002a:03116.B.
  • Nordström, K. Petersson, J. M. Smith: Martin-Löf's type theory. In: Handbook of logic in computer science, Vol. 5, 1-37, Oxford Univ. Press, 2000. Review No. 2002k:03015.
  • D. Fridlender: A proof-irrelevant model of Martin-Löf's logical framework. Math. Structures Comput. Sci. 12 (2002), no. 6, 771-795. Review submitted.
  • S. Valentini, Extensionality versus constructivity. Math. Log. Quaterly 48 (2002), no. 2, 179-187. Review No. 2002a:03116.
  • A. Beckmann, C. Pollett, R. Samuel: Ordinal notations and well-orderings in bounded arithmetic. Ann. Pure Appl. Logic 120 (2003), no. 1-2, 63-96. Review No. 2002a:03116.
  • R. Kahle Universes over Frege structures. Ann. Pure Appl. Logic 119 (2003), no. 1 -3, 191-223. Review submitted.
  • M. Rathjen: Realizing Mahlo set theory in type theory. Arch. Math. Log. 42 (2003), no. 1, 89 - 101. Review submitted.
  • S. Valentini: A Cartesian closed category in Martin -Löf's intuitionistic type theory. Theoret. Comput. Sci. 290 (2003), no. 1, 189-219. Review submitted.

Abstracts

• A. Setzer: Weakly final coalgebras in Martin-Löf type theory. Abstract for Logic Colloquium '08. To appear in Bulletin of Symbolic Logic. (postscript, pdf)
• A. Setzer: The role of large cardinals in ordinal notation systems. Abstract for Logic Colloquium '98. Bulletin of Symbolic Logic, 5:66-67, 1999. (pdf)
• A. Setzer: Why large cardinals are not needed for denoting small ordinals. Abstract for Logic Colloquium '97. Bulletin of Symbolic Logic, 4:72, 1998. (pdf-file)
• A. Setzer: Defining the least universe in Martin-Löf's type theory. Abstract for Logic Colloquium '96. Bulletin of Symbolic Logic, 3:276 - 277, 1997. (pdf-file, bibtex)
• A. Setzer: A type theory with one Mahlo universe. Abstract for Logic Colloquium 95. Bulletin of Symbolic Logic, 3:128 - 129, 1997. (pdf-file).
• A. Setzer: Proof theoretical strength of Martin-Löf Type Theory. Abstract for Logic Colloquium 1994. Bulletin of Symbolic Logic, 1:260, 1995. (pdf-file).

Drafts

• Fredrik Forsberg, Anton Setzer: Inductive-inductive Definitions. 10pp.
  • BibTeX
  • Draft Version
    • pdf
    • ps
    • dvi
• A. Setzer: Rules for the Pi_3-reflecting Universe, 1998. (postscript, pdf-file)
• A. Setzer:Wheels, 8 pp, 1997. (postscript, pdf-file)
• A. Setzer: An upper bound for the proof theoretical strength of Martin-Löf Type Theory with W-type and one Universe , 33pp, 1996. (postscript, pdf-file)
• A. Setzer: Set theoretical proofs as type theoretical programs. 10pp. Draft. (postscript, pdf-file).
• A. Setzer: A Model for a type theory with one Mahlo Universe, 10pp, 1996. (postscript, pdf-file,BibTeX-Entry)
• A. Setzer: A type theory for iterated inductive definitions, 14pp. , 1994. (postscript, pdf-file, Bib-Entry)

Slides of lectures

• Interactive programs in dependent type theory. Uppsala logic seminar, 1999. (pdf-file)
• Interactive programs in dependend type theory. Goeteborg doktorand course, 1999. (pdf-file).

Lecture Notes

• Logik MN2 (Logic 2 course) (postscript, pdf-file).
• HA^omega, constructive reals and lambda-calculus (Contains the later parts of the course "Constructive Mathematics and Lambda Calculus", postscript, pdf-file).

University Home | Computer Science Home
About the Department | Research | Teaching | Online Resources |