Official Homepage https://www.swansea.ac.uk/staff/a.g.setzer/ Administrative duties: Coordinator MSc in Advanced Computer Science and MSc in Advanced Software Technology Misc: General material related to Projects, Essays etc Software Maintainer of links to logic-servers world wide Further information on A. Setzer Links Anton Setzer's SPARK Ada Main Page (Lab Sessions) 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, Computational Foundry, Swansea University Bay Campus, Fabian Way, Swansea, SA1 8EN UK Visiting Address: Computational Foundry, Computer Science Department, 4th floor, room 403 ORCID: 0000-0001-5322-6060 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) More information: Further information on A. Setzer (research, other courses, links) can be found here Research Areas: 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 EP/G033374/1: Theory and Applications of Induction Recursion EPSRC Grant GR/S30450/01: Extension of Dependent Type Theory - Induction, Interaction, Universes Talks given: Slides of talks given Lecture notes Lecture Notes (pre 2016/17) Articles from PhD students and RAs Articles from PhD students and RAs Rare Articles Rare articles from others Back to academic staff at the Dep. of Computer Science

Publications of Anton Setzer

(Reportform, theses etc see below, slides of talks see here)

• Fahad Alhabardi and Anton Setzer: A simulator of Solidity-style smart contracts in the theorem prover Agda
  • To appear in Proceedings of ICBTA 2023, Xi'an, China, International Conference Proceedings Series by ACM (ISBN: 979-8-4007-0867-1), ACM Digital library.
  • BibTeX entry (to appear version)
  • pdf (Author's version)
• Peter Dybjer and Anton Setzer: The extended predicative Mahlo universe in Martin-Löf type theory
  • Journal of Logic and Computation, May 2023, exad022.
  • doi: 10.1093/logcom/exad022
  • BibTeX
  • pdf (Author's Version)
• Fahad Alhabardi and Anton Setzer: A model of Solidity-style smart contracts in the theorem prover Agda
  • In: 2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings), Mount Pleasant, MI, USA, 2023, pp. 1-10.
  • doi: 10.1109/AIBThings58340.2023.10292478
  • BibTeX
  • pdf (Author's Version)
• Fahad Alhabardi and Bogdan Lazar and Anton Setzer: Verifying Correctness of Smart Contracts with Conditionals
  • 2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain & Beyond (iGETblockchain). 2022, p 1- 6
  • BibTeX
  • pdf (Author's copy)
• Fahad Alhabardi, Arnold Beckmann, Bogdan Lazar and Anton Setzer: Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control
  • In: 27th International Conference on Types for Proofs and Programs (TYPES 2021) LIPIcs 239, 1:1--1:25, 2022.
  • https://drops.dagstuhl.de/opus/volltexte/2022/16770
  • doi: 10.4230/LIPIcs.TYPES.2021.1
  • BibTeX
  • pdf (Author's copy)
• Anton Setzer: Modelling Bitcoin in Agda
  • arXiv:1804.06398v1 [cs.CR], 17 April 2018.
  • BibTeX
  • Pdf (authors copy)
  • Pdf (ArXiv)
  • Agda Code (Git Repository)
• Stephan Adelsberger, Bashar Igried, Markus Moser, Vadim Savenkov and Anton Setzer: Formal Verification for Feature-based Composition of Workflows
  • In: Proceedings of SERENE 2018, 2018 14th European Dependable Computing Conference (EDCC), September 2018. doi 10.1109/EDCC.2018.00039
  • Demo of App created
  • BibTeX
  • pdf-file (Author's version)
  • Git repository
  • Agda code for viewing without installing Agda
• Stephan Adelsberger, Anton Setzer and Eric Walkingshaw: Developing GUI Applications in a Verified Setting In: Xinyu Feng and Markus Muller-Olm and Zijang Yang: Dependable Software Engineering. Theories, Tools, and Applications. Springer Lecture Notes in Computer Science 10998, doi 10.1007/978-3-319-99933-3_6.
  • Demo of App created
  • Proceedings of SETTA 18
  • BibTeX
  • pdf-file (Author's version)
  • Git repository
  • Agda code for viewing without installing Agda
• Stephan Adelsberger, Anton Setzer and Eric Walkingshaw: Declarative GUIs: Simple, Consistent, and Verified
  • In: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 18), 2018, pages 4:1 - 4:15. doi 10.1145/3236950.3236962
  • Demo of App created
  • BibTeX
  • pdf-file (Author's version)
  • Git repository
  • Agda code for viewing without installing Agda
• Ulrich Berger and Anton Setzer: Undecidability of Equality for Codata Types, doi 10.1007/978-3-030-00389-0_4
  • In: Corina Cirstea (Ed): Coalgebraic Methods in computer Science. Springer Lectuer Notes in Computer Science 11202, 2018.
  • Proceedings of CMCS'18
  • BibTeX
  • pdf-file (Author's version)
• Bashar Igried and Anton Setzer: Defining Trace Semantics in CSP-Agda
  • Accepted for publication in Postproceedings TYPES 2016. 23 pp.
  • BibTeX
  • pdf-file (Author's version)
• Andreas Abel, Stephan Adelsberger, Anton Setzer: Interactive Programming in Agda - Objects and Graphical User Interfaces
  • Journal of Functional Programming, 27, 2017. Doi 10.1017/S0956796816000319
  • Published Version
  • BibTeX
  • pdf-file (Author's version)
  • Git repository
• Bashar Igried and Anton Setzer: Trace and Stable Failures Semantics for CSP-Agda
  • In: Komendantskaya, Ekaterina and Power, John (Eds.): Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, Edinburgh, UK, 28-29 November 2016. Electronic Proceedings in Theoretical Computer Science 258, Open Publishing Association, 2017, pp. 36 - 51. doi 10.4204/EPTCS.258.3
  • Publishers Page
  • Published Version (open access)
  • BibTeX
  • pdf-file (Author's version)
• Bashar Igried and Anton Setzer: Programming with Monadic CSP-Style Processes in Dependent Type Theory
  • In Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016, Nara, Japan. ACM, 2016, pp. 28 -- 38. Doi 10.1145/2976022.2976032
  • Published Version
  • BibTeX
  • pdf-file (Author's version)
  • Workshop presentation
    • Video
    • Slides
• Anton Setzer: How to Reason Coinductively Informally.
  • In Reinhard Kahle, Thomas Strahm, Thomas Studer (Eds.): Advances in Proof Theory. Springer, 2016, pp. 377 -- 408. ISBN 978-3-319-29198-7. Doi 10.1007/978-3-319-29198-7_12
  • Published Version
  • BibTex
  • pdf-file (Author's Copy)
• Anton Setzer: The Use of Trustworthy Principles in a Revised Hilbert s Program.
  • In Kahle, Reinhard and Rathjen, Michael (Eds.): Gentzen's Centenary. Springer, 2015. ISBN 978-3-319-10102-6. Doi 10.1007/978-3-319-10103-3_3
  • Published Version
  • BibTex
  • pdf-file (Author's Copy)
• Karim Kanso, Anton Setzer: A light-weight integration of automated and interactive theorem proving.
  • Math. Struct. in Comp. Science, Online First, pp. 1 - 25, 2014. Doi 10.1017/S0960129514000140
  • Published Version
  • BibTeX
  • pdf-file (Author's Copy)
• Anton Setzer, Andreas Abel, Brigitte Pientka and David Thibodeau: Unnesting of Copatterns. In Gilles Dowek (Ed): Rewriting and Typed Lambda Calculi. Proceedings RTA-TLCA 2014. LNCS 8560, 2014, pp. 31 - 45. Doi 10.1007/978-3-319-08918-8_3
  • Published version
  • BibTeX
  • Pdf (Author's version)
• Philip James, Andy Lawrence, Faron Moller, Markus Roggenbach, Monika Seisenberger, Anton Setzer, Karim Kanso and Simon Chadwick: Verification of solid state interlocking programs
  • In: Steve Counsell and Manuel Núñez: Software Engineering and Formal Methods SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert, Madrid, Spain, September 23-24, 2013, Revised Selected Papers. LNCS 8368, 2014, pp. 253 - 268. Doi 10.1007/978-3-319-05032-4_19
  • Published Version
  • BibTex
  • Pdf (Author's version)
• Philip James, Andy Lawrence, Faron Moller, Markus Roggenbach, Monika Seisenberger, Anton Setzer, Karim Kanso and Simon Chadwick: Verification of solid state interlocking programs
  • In Stefan Gruner, Haxthausen, Anne Elisabeth, Tom Maibaum and Markus Roggenbach: FM-RAIL-BOK WORKSHOP 2013. Towards a formal methods body of knowledge for railway control and safety systems. Madrid, 23 Sept 2013, affiliated to SEFM'2013 11th International Conference on Software Engineering and Formal Methods, http://ssfmgroup.wordpress.com/
  • Proceedings of FM-RAIL-BOK WORKSHOP 2013
  • Published full report
  • BibTex
  • Pdf (Author's version)
• Neal Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg and Anton Setzer:Fibred Data Types
  • LICS 2013, pp. 243 -252. Doi: 10.1109/LICS.2013.30
  • Published Version
  • BibTeX
  • Pdf (Author's version)
• Andreas Abel, Brigitte Pientka, Anton Setzer and David Thibodeau: Copatterns: programming infinite structures by observations
  • Proceedings of POPL 2013, 2013, pp. 27 - 38. Doi 10.1145/2429069.2429075
  • Published version
  • BibTex
  • Author's version
• Fredrik Forsberg, Anton Setzer: Inductive-inductive Definitions. In: Ulrich Berger, Hannes Diener, Peter Schuster and Monika Seisenberger: Logic, Construction, Computation. Ontos mathematical logic 3, De Gruyter, 2012, pp. 259 -- 287, ISBN 9783110324921, doi: 10.1515/9783110324921.259
  • Published Version
  • BibTeX
  • Pdf (Author's version)
• Anton Setzer: Coalgebras as Types determined by their Elimination Rules
  • In: 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, 2012, pp. 351 -- 369, Doi: 10.1007/978-94-007-4435-6_16
  • Published version
  • Author's version
    • dvi
    • ps
    • pdf
    • BibTex
• Thorsten Altenkirch, Peter Morris, Fredrik Forsberg and Anton Setzer: A categorical semantics for inductive-inductive definitions.
  • In Corradini, Andrea and Klin, Bartek (Eds.) Algebra and Coalgebra in Computer Science. Proceedings of CALCO 2011, LNCS 6859, pp. 70 - 84. Doi 10.1007/978-3-642-22944-2_6
  • Published version
  • BibTeX
  • Author's version
    • Pdf
• Fredrik Nordvall Forsberg, Anton Setzer: Inductive-inductive Definitions.
  • In Anuj Dawar and Helmut Veith: CSL 2010. Proceedings. Lecture Notes in Computer Science, 454 - 468. Doi 10.1007/978-3-642-15205-4_35
  • BibTeX
  • Author's 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. ISBN: 978-3-86838-087-3, Doi 10.1515/9783110324907.315
  • Webpage with articles of the Festschrift
  • BibTeX
  • Author's 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
  • Author's version (dvi)
  • Author's 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. Doi 10.1007/978-3-7643-8653-5_16
  • BibTeX
  • Author's 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. Doi 10.1017/CBO9780511721151.009
  • BibTeX-Entry.
  • Author's 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
  • Author's 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. ISBN 978-184150-188-8.
  • BibTeX
  • Author's 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. Doi 10.1007/11874683_24
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Published Version
  • BibTeX
  • Author's version
    • Postscript
    • Pdf
• 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. ISBN 978-184150-188-8.
  • BibTeX
  • Author's version:
    • dvi file
    • Postscript
    • Pdf version
• Anton Setzer: Partial recursive functions in Martin-Löf 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. Doi 10.1007/11780342_51
  • Published Version by Springer
  • BibTeX
  • Author's version
    • dvi
    • ps
    • pdf
• Peter Dybjer, A. Setzer: Indexed Induction-Recursion. Long version.
  • Journal of Logic and Algebraic Programming 66, 1 - 49, 2006. Doi 10.1007/3-540-45504-3_7
  • BibTeX-Entry.
  • Published version
  • Author's 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. Doi 10.1016/j.entcs.2004.06.055
  • Published Version
  • BibTeX.
  • Author's 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 - 136. ISBN 9780198566519
  • BibTeX.
  • Author's 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
  • Author's version:
    • Postscript
    • Pdf
• Peter Dybjer, (Göteborg) and A. Setzer: Induction-Recursion and initial algebras. Annals of pure and applied logic, 124 (2003), 1 -- 47. Doi 10.1016/S0168-0072(02)00096-9
  • Published Version
  • BibTeX
  • Author's 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. Doi 10.1007/3-540-39185-1_16
  • BibTeX Entry
  • Published Version
  • Author's version:
    • dvi
    • postscript
    • pdf-file
• Peter 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. Doi 10.1007/3-540-45504-3_7
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Published Version
  • BibTeX.
  • Author's version
    • postscript.
    • pdf-file.
• 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. Doi 10.1007/3-540-44622-2_21
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Published Version
  • BibTeX.
  • Author's version
    • postscript.
    • pdf-file.
  • 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. Doi: 10.1007/s001530050140
  • Published Version
  • BibTeX Entry.
  • Author's 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. ISBN 1-56881-114-4
  • BibTeX.
  • Author's version:
    • dvi
    • postscript.
    • pdf-file.
• Peter 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. Doi 10.2307/2586750
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Published Version
  • BibTeX.
  • Author's version
    • postscript.
    • pdf-file.
• 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. Doi 10.2307/2586750
  • BibTeX
  • Published Version
  • Author's version:
    • pdf
• A. Setzer: Ordinal systems.
  • In B. Cooper and J. Truss (Eds.): Sets and Proofs, Cambridge University Press, Cambridge, pp. 301 - 331, 1999. ISBN 0-521-63549-7.
  • BibTeX
  • 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.
  • Author's 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. Doi 10.1016/S0168-0072(97)00078-X
  • BibTeX
  • Author's 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. ISBN: 978-0-19-850127-5
  • BibTeX
  • Author's version:
    • 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. Doi 10.1007/3-540-63385-5_50
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Published Version by Springer
  • BibTeX.
  • Author's version
    • 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. Doi 10.1007/3-540-63172-0_53
  • © Springer-Verlag. See as well Lecture Notes in Computer Science
  • Published Version by Springer
  • BibTeX.
  • Author's version
    • 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.
• A. Setzer: Ordinalzahlanalyse prädikativer Theorien unter Verwendung von Fundamentalfolgen. Master's Thesis, 116 pp., 1990.
  • postscript.
  • pdf-file.
  • BibTeX.

Reports, Submissions, Electronic Proceedings

• Bashar Igried and Anton setzer: Defining Trace Semantics for CSP-Agda
  • Submitted, 22 January 2017.
  • Pdf (Draft)
  • BibTeX
• 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
  • Author's 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.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 partial recursive functions in Martin-Löf type theory
  • Submitted.
  • dvi
  • ps
  • pdf
  • BibTeX
• 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/volltexte/2005/176/.
  • 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
• Peter 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.

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
  • Kachapova, F. A generalization of Beth model to functionals of high types. Proceedings of the 12th Asian Logic Conference, 185--209, World Sci. Publ., Hackensack, NJ, 2013. 03F55 (03B15). Review MR3289543 submitted.
  • 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.
  • Arnold 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

• Fahad Alhabardi and Anton Setzer: A simple model of smart contracts in Agda. In: Abstracts for Types 2023, 14 June 2023.
  • Abstract
  • Recording of talk
  • Slides
  • BibTeX entry
• 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

• Research Methodologies
  • BibTex