About
Dr Anton Setzer is a Reader in the Department of Computer Science, Swansea University.
Personal homepage: https://csetzer.github.io/
Dr Anton Setzer
Honorary Appointment (Science and Engineering)
Faculty of Science and Engineering
Available For Postgraduate Supervision
Research Links
Areas Of Expertise
- Interactive theorem proving
- Type theory
- Martin-Loef Type Theory
- Coinduction
- Proof theory
- Dependently typed programming
- Ordinals
- Pattern matching
Publications
Research Highlights
-
BRYANT, H., Seisenberger, M., Setzer, A., & Lawrence, A. (n.d.) Formal Assurance for Railway Signalling: Expanding SAT Proof Checking to Certify Z3's Inequality-Based SMT Proofs for ERTMS. Proceedings of International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation, ISoLA 2026. To appear in Lecture Notes in Computer Science SpringerSU Repository: https://cronfa.swan.ac.uk/Record/cronfa72334
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (n.d.) Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq. In RocqPL 2026ACM.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa71163
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (2025). Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda. In Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea (pp. 1-5). Zenodo.
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (2025). Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda. In Fredrik Nordvall Forsberg. (Ed.), Types 2025 (pp. 186-189).SU Repository: https://cronfa.swan.ac.uk/Record/cronfa70913
-
Setzer, A. (n.d.) Predicativity of the Mahlo Universe in type theory. Pillars of enduring strength: learning from Hermann Weyl Oxford University PressSU Repository: https://cronfa.swan.ac.uk/Record/cronfa69298
All Research
Journal Articles
-
Vessio, M., Beckmann, A., Roach, M., Saintier, S., Clements, R., & Setzer, A. (2024). InPerpetuity{Challenging Misperceptions of the Term ‘Smart Contract’}. European Journal of Law and Technology, 15(2)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa67545
-
Vessio, M., Beckmann, A., Roach, M., Saintier, S., Clements, R., & Setzer, A. (2024). InPerpetuity{Challenging Misperceptions of the Term “Smart Contract”}. European Journal of Law and Technology, 15(2)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa68617
-
Dybjer, P. & Setzer, A. (2024). The extended predicative Mahlo universe in Martin-Löf type theory. Journal of Logic and Computation, 34(6), 1032-1063.
-
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
-
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
-
BRYANT, H., Seisenberger, M., Setzer, A., & Lawrence, A. (n.d.) Formal Assurance for Railway Signalling: Expanding SAT Proof Checking to Certify Z3's Inequality-Based SMT Proofs for ERTMS. Proceedings of International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation, ISoLA 2026. To appear in Lecture Notes in Computer Science SpringerSU Repository: https://cronfa.swan.ac.uk/Record/cronfa72334
-
Setzer, A. (n.d.) Predicativity of the Mahlo Universe in type theory. Pillars of enduring strength: learning from Hermann Weyl Oxford University PressSU Repository: https://cronfa.swan.ac.uk/Record/cronfa69298
Conference Contributions
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (2025). Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda. In Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea (pp. 1-5). Zenodo.
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (2025). Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda. In Fredrik Nordvall Forsberg. (Ed.), Types 2025 (pp. 186-189).SU Repository: https://cronfa.swan.ac.uk/Record/cronfa70913
-
Dogan, H. & Setzer, A. (2025). SABEC: Secure and Adaptive Blockchain-Enabled Coordination Protocol for Unmanned Aerial Vehicles(UAVs) Network. In Proceedings of the 11th International Conference on Information Systems Security and Privacy (pp. 377-388). SCITEPRESS - Science and Technology Publications.
-
Alhabardi, F. & Setzer, A. (2023). A simulator of Solidity-style smart contracts in the theorem prover Agda. In Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications (pp. 1-11). ACM.
-
Alhabardi, F. & Setzer, A. (2023). 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) (pp. 1-10). IEEE.
-
Alhabardi, F., Lazar, B., & Setzer, A. (2022). Verifying Correctness of Smart Contracts with Conditionals. In 2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain & Beyond (iGETblockchain) (pp. 1-25). IEEE.
-
Alhabardi, F., Beckmann, A., Lazar, B., & Setzer, A. (2022). Verification of Bitcoin Script in Agda using Weakest Preconditions for Access Control. In Henning Basold, Jesper Cockx, Silvia Ghilezan (Ed.), 27th International Conference on Types for Proofs and Programs (TYPES 2021) (pp. 1:1-1:25). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
-
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.
-
Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Developing GUI Applications in a Verified Setting. In Dependable Software Engineering. Theories, Tools, and Applications (pp. 89-107). Springer International Publishing.
-
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
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (n.d.) Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq. In RocqPL 2026ACM.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa71163
Supervision
-
An Investigation into Applications of User-Propagators for the Z3 SMT Solver (current)
PhDOther supervisor: Prof Markus Roggenbach -
Proof Checking for SMT-Solving and its application in the Railway Domain (current)
PhDOther supervisor: Dr Monika Seisenberger -
Overcoming Information Silos: Semantic AI for Intelligent Interoperability in Pharmaceutical Supply Chains (current)
PhDOther supervisor: Prof Arnold Beckmann -
Verification of Smart contracts using the interactive theorem prover Agda (awarded 2024)
PhDOther supervisor: Prof Arnold Beckmann -
Secure Identity Management System in Unmanned Aerial Vehicles Network (awarded 2025)
PhDOther supervisor: Dr Phillip James