About
Dr Anton Setzer is a Reader in the Department of Computer Science, Swansea University.
Dr Anton Setzer
Reader,
Computer Science
Telephone number
+44 (0) 1792 513368
Research Links
Available For Postgraduate Supervision
Areas Of Expertise
- Interactive theorem proving
- Type theory
- Martin-Loef Type Theory
- Coinduction
- Proof theory
- Dependently typed programming
- Ordinals
- Pattern matching
Publications
Research Highlights
-
Berger, U., Matthes, R., & Setzer, A. (2019). Martin Hofmann’s case for non-strictly positive data types. In Leibniz International Proceedings in Informatics, LIPIcs
-
Setzer, A. (2019). An Upper Bound for the Proof Theoretic Strength of Martin-Löf Type Theory with W-type and one Universe. SpringerSU Repository: https://cronfa.swan.ac.uk/Record/cronfa51297
-
Adelsberger, S., Igried, B., Moser, M., Savenkov, V., & Setzer, A. (2018). Formal Verification for Feature-Based Composition of Workflows. (pp. 173-181). SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems.
-
Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Developing GUI Applications in a Verified Setting. Dependable Software Engineering. Theories, Tools, and Applications (pp. 89-107). Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018
-
Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Declarative GUIs: Simple, Consistent, and Verified. In PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (pp. 1-15). Proceedings of PPDP 2018.
All Research
Journal Articles
-
Igried, B. & Setzer, A. (2018). Defining Trace Semantics for CSP-Agda. Leibniz International Proceedings in Informatics, LIPIcs, 97, 12:1-12:23.
-
Igried, B. & Setzer, A. (2017). Trace and Stable Failures Semantics for CSP-Agda. Electronic Proceedings in Theoretical Computer Science, 258, 36-51.
-
Abel, A., Adelsberger, S., & Setzer, A. (2017). Interactive programming in Agda – Objects and graphical user interfaces. Journal of Functional Programming, 27
-
Kanso, K. & Setzer, A. (2014). A light-weight integration of automated and interactive theorem proving. Mathematical Structures in Computer Science, 26(01), 129-153.
-
Kanso, K., Moller, F., & Setzer, A. (2009). Automated Verification of Signalling Principles in Railway Interlocking Systems. Electronic Notes in Theoretical Computer Science, 250(2), 19-31.
-
Kanso, K., Moller, F., & Setzer, A. (2009). Automated Verification of Signalling Principles in Railway Interlocking Systems. Electronic Notes in Theoretical Computer Science, 250(2), 19-31.
-
Abdul Rauf, R., Berger, U., & Setzer, A. (2008). A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++. Theory of Computing Systems, 43(3-4), 298-321.
-
Dybjer, P. & Setzer, A. (2006). Indexed induction–recursion. The Journal of Logic and Algebraic Programming, 66(1), 1
-
Dybjer, P. & Setzer, A. (2003). Induction–recursion and initial algebras. Annals of Pure and Applied Logic, 124(1-3), 1-47.
Book Chapters
-
Setzer, A. (2019). An Upper Bound for the Proof Theoretic Strength of Martin-Löf Type Theory with W-type and one Universe. SpringerSU Repository: https://cronfa.swan.ac.uk/Record/cronfa51297
-
Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Developing GUI Applications in a Verified Setting. Dependable Software Engineering. Theories, Tools, and Applications (pp. 89-107). Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018
-
Setzer, A. (2016). How to Reason Coinductively Informally. Advances in Proof Theory-408). Birkhäuser
-
Setzer, A. (2015). The Use of Trustworthy Principles in a Revised Hilbert’s Program. Gentzen's Centenary (pp. 45-60). Springer
-
Setzer, A. (2012). Coalgebras as Types Determined by Their Elimination Rules. Epistemology versus Ontology (pp. 351-369).
-
Nordvall Forsberg, F. & Setzer, A. (2010). Inductive-Inductive Definitions. Computer Science Logic (pp. 454-468). Springer
-
Kahle, R. & Setzer, A. (2010). An extended predicative definition of the Mahlo universe. Ways of Proof Theory (pp. 309-334). De Gruyter
-
Setzer, A. (2008). Universes in type theory part I—Inaccessibles and Mahlo. Logic Colloquium 2004 (pp. 123-156). Cambridge University Press
-
Setzer, A. (2008). Proof theory and Martin-Löf Type Theory. One Hundred Years of Intuitionism (1907–2007) (pp. 257-279). Birkhäuser
Conference Contributions
-
Berger, U., Matthes, R., & Setzer, A. (2019). Martin Hofmann’s case for non-strictly positive data types. In Leibniz International Proceedings in Informatics, LIPIcs
-
Adelsberger, S., Igried, B., Moser, M., Savenkov, V., & Setzer, A. (2018). Formal Verification for Feature-Based Composition of Workflows. (pp. 173-181). SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems.
-
Berger, U. & Setzer, A. (2018). Undecidability of Equality for Codata Types. In Coalgebraic Methods in Computer Science (pp. 34-55). Springer International Publishing.
-
Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Declarative GUIs: Simple, Consistent, and Verified. In PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (pp. 1-15). Proceedings of PPDP 2018.
-
Igried, B. & Setzer, A. (2016). Programming with monadic CSP-style processes in dependent type theory. In TyDe 2016 (pp. 28-38). ACM.
-
Setzer, A., Abel, A., Pientka, B., & Thibodeau, D. (2014). Unnesting of Copatterns. In Rewriting and Typed Lambda Calculi (pp. 31-45). Springer.
-
James, P., Lawrence, A., Moller, F., Roggenbach, M., Seisenberger, M., Setzer, A., Kanso, K., & Chadwick, S. (2014). Verification of Solid State Interlocking Programs. In Software Engineering and Formal Methods-268).
-
Abel, A., Pientka, B., Thibodeau, D., & Setzer, A. (2013). Copatterns: programming infinite structures by observations. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 27-38). ACM, New York, NY, USA.
-
Ghani, N., Malatesta, L., Forsberg, F., & Setzer, A. (2013). Fibred Data Types. In Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on (pp. 243-252). IEEE.
-
Altenkirch, T., Morris, P., Forsberg, F., & Setzer, A. (2011). A Categorical Semantics for Inductive-Inductive Definitions. In Algebra and Coalgebra in Computer Science. 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings (pp. 70-84). Springer.
-
Kanso, K. & Setzer, A. (2009). Specifying railway interlocking systems. (pp. 233-236). Swansea University.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa106
-
Harwood, W., Moller, F., & Setzer, A. (2006). Weak Bisimulation Approximants. In Computer Science Logic (pp. 365
Supervision
-
Verification of Smart contracts using the interactive theorem prover Agda (current)
PhDOther supervisor: Prof Arnold Beckmann -
'''Application of Proof-theoretic Methods to Natural Language Processing''' (awarded 2018)
PhDOther supervisor: Dr Monika SeisenbergerOther supervisor: Dr Ulrich Berger -
'Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification.' (awarded 2018)
PhDOther supervisor: Dr Ulrich Berger -
First Steps Towards Computable Frame Theory (current)
MResOther supervisor: Dr Arno Pauly -
'Logic and Computation (Testing Software Product Lines)' (awarded 2017)
MResOther supervisor: Prof Markus Roggenbach
Taught Modules
-
CSC313 High Integrity Systems
This module introduces various techniques for developing high integrity systems.
-
CSCM10 Computer Science Project Research Methods
This module will introduce students to some fundamental research methodologies and good practice in research. They will undertake background research including a literature review and specify the aims of their MSc project.
-
CSCM10J Computer Science Project Research Methods
This module will introduce students to some fundamental research methodologies and good practice in research. They will undertake background research including a literature review and specify the aims of their MSc project.
-
CSCM13 Critical Systems
This module introduces techniques for developing critical systems, especially safety critical systems. Students will gain experience in applying modern tools in the development of critical software.
-
CSCM29 Blockchain, Cryptocurrencies and Smart Contracts
This is a module on modern blockchain technology and its major applications. It will give an overview on the technological setup of major cryptocurrencies, and introduce the blockchain as a concept for determining the order of events in a distributed database. In addition, it will discuss the implementation of smart contracts and summarise the current state of the art of security issues in cryptocurrencies, blockchain technology, and smart contracts.
-
CSMM29 Blockchain, Cryptocurrencies and Smart Contracts
This is a module on modern blockchain technology and its major applications. It will give an overview on the technological setup of major cryptocurrencies, and introduce the blockchain as a concept for determining the order of events in a distributed database. In addition, it will discuss the implementation of smart contracts and summarise the current state of the art of security issues in cryptocurrencies, blockchain technology, and smart contracts.