About
Dr Anton Setzer is a Reader in the Department of Computer Science, Swansea University.
Personal homepage: https://csetzer.github.io/
Dr Anton Setzer
Reader
Computer Science
Office - 403
Fourth Floor
Computational Foundry
Bay Campus
Fourth Floor
Computational Foundry
Bay Campus
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
-
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.
-
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
-
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
All Research
Journal Articles
-
Vessio, M., Beckmann, A., Roach, M., Saintier, S., Clements, R., & Setzer, A. (2024). In Perpetuity {Challenging Misperceptions of the Term ‘Smart Contract’}. European Journal of Law and Technology, 15(2)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa67545
-
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
Conference Contributions
-
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
Supervision
-
SMT Solving for Graph-Theoretic Representations of Railway Systems (current)
PhDOther supervisor: Dr Monika Seisenberger -
Proof Checking for SMT-Solving and its application in the Railway Domain (current)
PhDOther supervisor: Dr Monika Seisenberger -
Semantic Technologies for Addressing Challenges 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 (current)
PhDOther supervisor: Dr Phillip James
Taught Modules
-
CSC313 High Integrity Systems
This module introduces various techniques for developing high integrity systems.
-
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.