Theses, Articles, Drafts and Lecture Notes of Anton Setzer

Theses

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

Publications

(Preprints see "Reports" below)

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
- 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).
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.
- Postscript version
- pdf-version
A. Setzer: Extending Martin-Löf Type Theory by one Mahlo-Universe.
- Arch. Math. Log (2000), 39: 155 - 181.
- Postscript version
- 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 version.
- 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.
A. Setzer: Ordinal systems.
- In B. Cooper and J. Truss (Eds.): Sets and Proofs, Cambridge University Press, Cambridge, pp. 301 -- 331, 1999.
- Some mistakes have been detected. Here are the corrections:
  - Corrections (postscript, pdf).
  - Corrected version of Ordinal Systems
  - Postscript-version.
  - pdf-file.
  - Some people have problems with printing this file, therefore here is the Latex-source
A. Setzer: Well-ordering proofs for Martin-Löf Type Theory with W-type and one Universe.
- Preliminary version. The final (slightly changed) version has appeared in Annals of Pure and applied Logic, 92 (1998), 113 -- 159.
- postscript.
- pdf-file.
- Reviewed in Bulletin of Symbolic Logic, Vol. 6, Number 4, Dec 2000, pp. 478 - 479
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.
- pdf-file
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.
- Postscript-version
- 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
- Postscript Version
- 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
- Postscript Version
- pdf-file

Reports, Submissions, Electronic Proceedings

Peter Hancock, Anton Setzer: Interactive programs in type theory
- Workshop on subtyping and dependent types in programming, Ponte de Lima, Portugal, 7 July 2000
- pdf-file
P. Dybjer, (Göteborg) and A. Setzer: Induction-Recursion and initial algebras.
- Postscript version (Diagrams look better in the postscript version).
- pdf-file
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.
- 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-Version
- pdf-file

Reviews

Review of Troelstra, A.S.; Schwichtenberg, H.: Basic proof theory. Zentralblatt MATH, 957.03053.
Review of S. Tupailo: Finitary reductions for local predicativity I: Recursively regular ordinals. Zentralblatt MATH, 949.03053.
A. Setzer: Review of J. Roger Hindley, Basic simple type theory, Bull. Sym. Log., 64, 4: 1832 - 1833, 1999
More to come.

Abstracts

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-file)
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)
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

A. Setzer: Rules for the Pi_3-reflecting Universe, 1998. (postscript, pdf)
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)
A. Setzer: A type theory for iterated inductive definitions, 14pp. , 1994. (postscript, pdf-file)

Slides of lectures

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

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).