Publications EPSRC Grant GR/S30450/01

List of publications written during the EPSRC project: Extension of Dependent Type Theory - Induction, Interaction, Universes

• Back to Project home page

• [ABS07a] Rose H. Abdul Rauf, Ulrich Berger, Anton Setzer: Functional Concepts in C++
  • To appear in Post-symposium Proceedings of TFP 2006. Series Trends in Functional Programming, Intellect, 2007.
  • dvi file
  • Postscript
  • Pdf version
  • BibTeX
• [ABS07b] Rose H. Abdul Rauf, Ulrich Berger, Anton Setzer: A provably correct translation of the $\lambda$-calculus into a mathemetical model of C++
  • Invited submission to J Theo Comp Sys, 2007. (Refereed post proceedings of the conference CiE 2006).
  • dvi file
  • Postscript
  • Pdf version
  • BibTeX
• [AR07] Rose H. Abdul Rauf: Functional Concepts in C++. PhD thesis, Dept. of Computer Science, University of Wales Swansea, UK, 2007, in preparation.
• [HM07] Magne Haveraaen, Markus Michelbrink: A direct translation of the simply typed lambda calculus into C++-templates. Submitted to Journal of Functional Programming, 2007.
• [MS07] Markus Michelbrink: Exact Dickson Ordinals
  • Draft, 2007.
  • Postscript
  • Pdf
  • BibTeX
• [Se07a] Anton Setzer: Object-oriented programming in dependent type theory
  • To appear in Post-symposium Proceedings of TFP 2006. Series Trends in Functional Programming, Intellect, 2007.
  • dvi file
  • Postscript
  • Pdf version
  • BibTeX
• [Se07b] Anton Setzer: Universes in Type Theory Part II -- Autonomous Mahlo and Pi_3-Reflection.
  • 32 pages, submitted, 2007.
  • dvi
  • postscript
  • pdf-file
  • BibTeX-Entry
• [Se07c] Anton Setzer: A data type of partical recursive functions in Martin-Löf type theory
  • 35 pp. Invited submission to J Log Comp. (Post proceedings of the conference CiE 2006), 2007.
  • dvi
  • ps
  • pdf
  • Bibtex-entry
• [ABS06] 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
• [AR06] Rose Hafsah Abdul Rauf: Integrating Functional Programming into C++: Implementation and Verification.
  • In: A. Beckmann, Ulrich Berger, B. Löwe, J. Tucker: Logical Approaches to Computational Barriers. Conference CiE 2006. Report No. CSR 7-2006, Department of Computer Science, University of Wales Swansea, pp. 2 -- 11, 2006. (Refereed Proceedings).
  • Pdf file of the complete report
  • postscript.
  • pdf-file.
  • BibTeX-Entry.
• [DS06] P. Dybjer, A. Setzer: Indexed Induction-Recursion. Long version.
  • Journal of Logic and Algebraic Programming 66, 1 - 49, 2006.
  • Published version via DOI
  • postscript.
  • pdf-file.
  • BibTeX-Entry.
• [HMS06] 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.
  • Copyright Springer-Verlag. See as well Lecture
  • Get article from Springer using DOI
  • Postscript
  • Pdf
  • BibTeX
• [Mi06a]Markus Michelbrink: Interfaces as games, programs as strategies
  • In: Jean-Christophe Filliatre, Christine Paulin, Benjamin Werner, ed.: Types for Proofs and Programs (TYPES 2004).
  • Final Version available from Springer
  • postscript.
  • pdf-file.
  • BibTeX.
• [Mi06b]Markus Michelbrink: Interfaces as Functors, Programs as Coalgebras - a Final Coalgebra Theorem in Intensional Type Theory
  • In Theor. Compu. Sci., Vol. 360, Issue 1 (August 2006), pp. 415 - 319.
  • Access via DOI
  • postscript.
  • pdf-file.
  • BibTeX.
• [Mi06c] Markus Michelbrink: A generalisation of Hancock-Setzer Interfaces
  • Draft.
• [Mi06d]Markus Michelbrink A Buchholz derivation system for the ordinal analysis of KP+ $\Pi_3$-reflection
  • J. Symbolic Logic, 71 (4), 2006, pp. 1237 - 1283.
  • postscript.
  • pdf-file.
  • BibTeX.
• [Se06a] Anton Setzer: Object-oriented programming in dependent type theory
  • In conference proceedings of TFP 2006, 2006.
  • dvi file
  • Postscript
  • Pdf version
  • BibTeX
• [Se06b] Anton Setzer: Partial recursive functions in dependent type theory
  • Copyright Springer-Verlag. See as well Lecture Notes in Computer Science
  • In: Arnold Beckmann, Ulrich Berger, Benedikt L{\"o}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
• [Se06c] A. Setzer: Universes in Type Theory I -- Inacccessibles and Mahlo
  • In: A. Andretta, K. Kearnes and D. Zambella: Logic Colloquium '04. Association of Symbolic Logic, Lecture Notes in Logic, 29, 2006, pp. 123 - 156.
  • postscript.
  • pdf-file.
  • BibTeX-Entry.
• [HS05a] 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.
  • dvi (diagrams don't show well; use ps or pdf instead).
  • postscript.
  • pdf-file.
  • BibTeX.
• [HS05b] 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.
• [MS05]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
  • postscript.
  • pdf-file.
  • BibTeX.
• [Se04] A. Setzer: Proof Theory of Martin-Löf Type Theory -- An Overview.
  • Mathematiques et Sciences Humaines, 42 année, 165, 2004, p. 59--99.
  • Postscript
  • Pdf
  • BibTex
• [DS03] 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).
  • dvi Version (Diagrams look better in the postscript version).
  • postscript.
  • pdf-file
  • BibTeX-entry
• [Se03] A. Setzer: Java as a functional programming language.
  • Copyright 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.
  • postscript
  • pdf-file
  • BibTeX Entry

• Back to Project home page