Contact:
Dr Monika Seisenberger
Dept. of Computer
Science
School of Mathematics and Computer Science
Faculty of Science and Engineering
Swansea
University
Bay Campus, Fabian Way
Swansea SA18EN, UK
f: (+44) (0)1792 295708
e: m.seisenberger@swansea.ac.uk
Dr Monika Seisenberger
Associate Professor in Computer Science
Deputy Head of Department
Research:
Modelling, Verification, Formal Methods, Verification of Railway Control Systems, Trustable AI systems; Logic, Interactive Theorem Proving, Proof Theory, in particular Computational Content of Proofs; Program extraction, program verification.
I am the head of Swansea's Theoretical Computer Science group and a member of the Swansea Railway Verification Group.
Research Projects:- CID, Computing with Infinite Data, Horizon2020, April 2017-March 2022 (Co-PI)
- CORCON, Correctness by Construction, Jan 2014- Dec 2017 (PI) FP7 Marie Curie International Research Project, PIRSES-GA-2013-61xs2638, This is a project which involved researchers from Japan, Australia, New Zealand, USA, India, Korea, Sweden, Italy, Germany, and UK and specifically supports and offers training for PhD students.
- COMPUTAL, Computable Analysis FP7 Marie Curie International Research Project, PIRSES-GA-2011-294962, Febr 2012- Jan 2016 (Member)
- Andrew Lawrence (Program Extraction, Verification of Railway Control Systems), completed 2016
- Alison Jones (Proof theoretic methods in Natural Language Processing), completed 2018
- Sulaiman Al-Shekaili (Analyzing Organizational Networks, Cyberterrorism), MSc by Research, completed 2018
- Jay Morgan, Trustable Machine Learning Systems, ML and Verification, Start September 2018
- Arved Friedemann, Prooftheory and Complexity Theory, Start September 2018
- Aled Walters, Verification and Testing of Train Control Systems, Start September 2018
Conferences and workshops I am/was involved in:
- CiE 2022, Swansea, 11-15 July 2022 (PC member)
- BCTCS 2022, Swansea, 11-13 April 2022 (Co-chair)
- CCC 2021, Birmingham, September 2021 (invited speaker)
- ASL Logic Colloquium, Poznan, 19-24 July 2021, Organizer of Special Session "Proofs and Programs"
- BCTCS 2020, Swansea, 6-8 April 2020
- Proof theory summer school and workshop, Swansea, September 2019 (Co-organizer, PC member)
- CCC 2019, Ljubljana, CID project workshop (Swansea representative)
- CLMPST 2019, Prague (Invited speaker)
- LCC 2019, Patras (PC Co-chair)
- SACLA 2019, SA (PC member)
- CiE 2018, Kiel (PC member and Invited Speaker at Women in Computability Workshop)
- Hausdorff Research Institute, Bonn, (Invited Researcher), 24/7-24/8/2018
- ASL North American Logic Conference 2017, Boise, (Invited Plenary Speaker)
- ITP 2017 (PC member)
- BLC 2017, Brighton (PC member)
- Well-quasiorderings in Computer Science, Dagstuhl seminar, 17-22 Jan 2016 (Co-organizer)
- Well-quasiorderings: From Theory to Applications, Minisymposium at DMV 2015, 21-25 Sept 2015, Hamburg, (Co-organizer)
- Continuity, Computatiblity, Constructivity, CCC2015, Munich/Kochel, 14-18 Sept 2015 (Co-organizer, PC member)
- CALCO 2015 (PC member)
- Continuity, Computability, Constructivity, CCC2014, Ljubljana, 8-13 September 2014 (PC member).
- Classical Logic and Computation 2014, Vienna, 13 July 2014 (PC member)
- Correctness by Construction, CORCON 2014 Workshop, Genua, 24-27 March 2014 (Organization Committee Member)
- Coalgebraic Methods in Computer Science, CMCS 2014 Grenoble, 5-6 April 2014 (PC member)
- CCC2013, 26-30 June 2013, Swansea/Gregynog, Wales (PC member, Co-organizer)
- CALCO Early Ideas 2013, Warsaw (PC chair)
- CALCO 2013, Warsaw (PC member)
- 19th Wessex Theory Seminar Meeting, 24 January 2013, Swansea (Organizer)
- Domains X Workshop 2011, 5-7 September 2011, Swansea (Co-organizer)
- CALCO Young Researchers Workshop, CALCO-jnr 2011, 29 August 2011, Winchester (PC chair)
- Program Extraction and Constructive proofs, Workshop in honor of Helmut Schwichtenberg, 21-22 August 2010, Brno, Czech Republic (Co-organizer)
- BCSWomen Lovelace Colloquium 2010 8 April 2010, Cardiff (PC member)
- 4th Wessex Theory Seminar Meeting, 29 October 2009, Swansea (Organizer)
- British Logic Colloquium 2009, 3-5 September 2009, Swansea (Co-organizer)
- CALCO Young Researchers Workshop, CALCO-jnr 2009, 6 September 2009, Udine, Italy (PC member)
- 3rd Wessex Theory Seminar Meeting, 3 March 2009, Bath, and 4 March 2009, Swansea (Co-organizer)
- Proof, Computation, Complexity, PCC 2008, 8-9 August 2008, Oslo (PC member)
- Formalising Mathematics and Extracting Algorithms from proofs, CiE2008, 15-20 June 2008, Athens (Special session organizer)
- Russell'08, Proof Theory meets Type Theory,15-16 March 2008, Swansea (Co-organizer)
- CALCO Young Researchers Workshop, CALCO-jnr 2007, 20 August 2007, Bergen (PC member)
- Proof, Computation, Complexity, PCC 2007, 13-14 April 2007, Swansea (Co-organizer) Proof theorists on the beach, further photographs from PCC 2007.
- Computability in Europe, CiE 2006, 30 June - 5 July 2006, Swansea (Co-organizer) conference photo.
- CALCO Young Researchers Workshop, CALCO-jnr 2005, 2 September 2005, Swansea, (PC member, Co-organizer) Day0, CALCO-jnr talks, beach party, excursion, all photographs (by Will Harwood).
Industrial Collaboration:
- Siemens Rail Automation, Chippenham, UK,
-
Teaching:
- CS-081 Computational Problem Solving, Spring 2020 (In Python)
- CS-205 Declarative Programming, 2021/2022, since 2012, (In Haskell and Prolog)
- CS-081 Programming with Algorithms and Data Structures, (in Python), 2013-2018
- CS-161 Introduction to Computing I, 2005-2011, 2012/13
- CS-171 Introduction to Computing II, 2006-2011 (in Java)
- CS-141 Programming - Principles and Practice 2010-2011 (in Java)
- CS-318 Cryptography and IT-Security/ CS-M18 IT-Security: Theory and Practice, 2005-2009
- CS-313 High Integrity Systems/ CS-M13 Critical Systems, 2006-2008 (in Spark Ada)
- CS-332 Designing Algorithms/ CS-M32 Algorithm Design and Analysis, 2004-2008
- CS-151 Introduction to Computing, 2004/2005 (in Java)
- CS-226 Computability theory, 2004/2005
- CS-213 System Specification, 2004-2011 (in Maude)
Please find more detailed information, course material, and grades on Blackboard.
Administration:
- Deputy Head of the Department of Computer Science (2017-now)
- Programme Director in Computer Science (Jan 2015-2021) - As Programme Director in I am responsible for all undergraduate and postgraduate programmes in Computer Science.
- Head of Yr2 (2012-Dec 2014)
- Examination officer (examination papers), 2004-July 2011
- Disability/Special Needs officer for the department of Computer Science, Disability link tutor for the School of Physical Sciences, 2004- July 2011
- Student Enrolment officer, 2006- July 2011
- Head of Foundation Year, 2008- July 2011
Refereed Journal and Conference Publications, Invited Publications, PhD-thesis, Edited Proceedings:
- Peter Schuster, Monika Seisenberger, Andreas Weiermann, Well-Quasi Orders in Computation, Logic, Language and Reasoning, Trends in Logic 53, Springer, 2020
- Ulrich Berger, Phillip James, Andrew Lawrence, Markus Roggenbach, Monika Seisenberger, Verification of the European Rail Traffic Management System in Real-Time Maude. Science of Computer Programming 154, pp.66-81, 2018.
- Ulrich Berger, Alison Jones, Monika Seisenberger, Program Extraction Applied to Monadic Parsing, Journal of Logic and Computation, Volume 29, Issue 4, Pages 487–518, 2019, https://doi.org/10.1093/logcom/exv078.
- Jay Morgan, Adeline Paiement, Monika Seisenberger, Jane Williams, Adam Wyner, A Chatbot Framework for the Children’s Legal, Centre Frontiers in Artificial Intelligence and Applications, Volume 313, Jurix 2018, pp. 205--209, 2018.
- Phillip James, Andrew Lawrence, Markus Roggenbach, Monika Seisenberger, Towards Safety Analysis of ERTMS/ETCS Level 2 in Real-Time Maude, Formal Techniques for Safety-Critical Systems, 2015, CCIS, volume 596, 2016
- Helmut Schwichtenberg, Monika Seisenberger, Franziskus Wiesnet, Higman's Lemma and its Computational Content, Advances in Proof theory, pp 353--375, 2016
- Ulrich Berger, Andrew Lawrence, Fredrik Nordvall Forsberg, and Monika Seisenberger, Extracting verified decision procedures: DPLL and Resolution, Logical Methods in Computer Science, LMCS-11(1:6), 2015
- Ulrich Berger, Alison Jones, and Monika Seisenberger, Program Extraction Applied to Monadic Parsing, International workshop at the Vienna Summer of Logic, Second Workshop on Natural Language and Computer Science 2014, NLCS 2014.
- Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods, Extracting Imperative Programs from Proofs: In-place Quicksort, in Ralph Matthes and Aleksy Schubert, eds., 19th International Conference on Types for Proofs and Programs (TYPES 2013), vol. 26 of Leibniz International Pro- ceedings in Informatics (LIPIcs), pp. 84--106, Schloss Dagstuhl{Leibniz- Zentrum fuer Informatik, Dagstuhl, Germany, 2014. doi:http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.84, URL http://drops.dagstuhl.de/opus/volltexte/2014/4627
- Phillip James, Andy Lawrence, Faron Moller, Markus Roggenbach, Monika Seisenberger, Anton Setzer, Karim Kanso, and Simon Chadwick, Verifica- tion of solid state interlocking programs, in Steve Counsell and Manuel Nez, eds., Software Engineering and Formal Methods, Lecture Notes in Computer Science, pp. 253{268, Springer International Publishing, ISBN 978-3-319-05031-7, 2014. doi:10.1007/978-3-319-05032-4 19, URL http: //dx.doi.org/10.1007/978-3-319-05032-4_19
- Bartek Klin and Monika Seisenberger, CALCO Early Ideas 2013, Selected Papers, 2014.
- Philip James, Andy Lawrence, Faron Moller, Markus Roggenbach, Monika Seisenberger, Anton Setzer, Karim Kanso, and Simon Chadwick, Verification of solid state interlocking programs. Accepted for FM-RAIL-BOK WORKSHOP 2013, Towards a formal methods body of knowledge for railway control and safety systems, Madrid, 23 Sept 2013, affiliated to SEFM'2013 11th International Conference on Software Engineering and Formal Methods, 2013
- U. Berger, H. Diener, P. Schuster, M. Seisenberger (editors), Logic, Construction, Computation, Ontos Mathematical Logic 3, Ontos Verlag, 2012
- U. Berger, A. Lawrence, M. Seisenberger, Extracting a DPLL Algorithm, MFPS 2012, Electronic Notes in Theoretical Computer Science 286 (2012), pp. 243-256, dx.doi.org/10.1016/j.entcs.2012.08.016
- C. Cirstea, M. Seisenberger, T. Wilkinson (editors), CALCO Young Researchers Workshop, CALCO-jnr 2011, Selected Papers, Eprint 336337, University of Southampton, 2012.
- U. Berger, M. Seisenberger, Proofs, Programs, Processes, Theory of Computing, Volume 51, Number 3 (2012), 313-329 (Journal version, 17 pages), Doi:10.1007/s00224-011-9325-8
- U.Berger, K. Miyamoto, H. Schwichtenberg, M. Seisenberger, Minlog - A Tool for Program Extraction for Supporting Algebra and Coalgebra, CALCO-Tools 2011, LNCS 6859, pp. 393-399, 2011. Doi:10.1007/978-3-642-22944-2_29
- A. Lawrence, M. Seisenberger, Verification of Railway Interlockings in Scade, AVoCS 2010.
- U. Berger, M. Seisenberger, Proofs, Programs, Processes, CiE 2010, LNCS 6158 , pp. 39-48, 2010, Doi: 10.1007/978-3-642-13962-8_5 (conference version, 10 pages)
- M. Haveraaen, M. Lenisa, J. Power, M.Seisenberger, editors, CALCO Young Researchers Workshop, CALCO-jnr 2009, Selected papers, Udine, September 2009, Report no 5-2010, Universita di Udine, 2010.
- U. Berger, M. Seisenberger, Program Extraction via Typed Realisability for Induction and Coinduction, In: Pohlers Festschrift, 2010. (Invited.) (Contains also the proof that termination of the extracted programs is guaranteed.)
- M. Seisenberger, Efficient Synthesis of Exact Real Number Algorithms, In: A. Beckmann, C.Gassner and B. Lowe, Proceedings of Logical Approaches to Barriers in Computing and Complexity, Greifswald, 2010, 163--167 (Invited).
- M. Seisenberger, Program Verification via Extraction from Coinductive Proofs. AvoCS 2009, Short Contribution, 2009.
- M. Seisenberger, Programs from Proofs using Classical Dependent Choice. Annals of Pure and Applied Logic, Vol 153/1-3, pp 97-110, 2008.
- M. Haveraaen, J. Power, M. Seisenberger, editors, CALCO Young Researchers Workshop, CALCO-jnr 2007, Selected papers, Bergen, August 2007, University of Bergen, UIB report no 2008-367, 2008.
- S. Fincher, D.Barnes,P. Bibby, J. Bown, V. Bush, P. Campbell, Q. Cutts, S. Jamieson, T. Jenkins, M. Jones, D. Kazakov, T. Lancaster, M. Ratcliffe, M. Seisenberger, D. Shinner-Kennedy, C. Wagstaff, L. White, and C. Whyley, Some Good Ideas from the Disciplinary Commons. In: Proceedings of the 7th Annual Conference of the ICS HE Academy, Dublin, August 2006, pages 153--158.
- Q. Cutts, S. Fincher, D. Barnes, P. Bibby, J. Bown, V. Bush, P. Campbell, S. Jamieson, T. Jenkins, M. Jones, D. Kazakov, T. Lancaster, M. Ratcliffe, M. Seisenberger, D. Shinner-Kennedy, C. Wagstaff, L. White, and C. Whyley, Laboratory Exams in First Programming Courses. In: Proceedings of 7th Annual Conference of the ICS HE Academy, Dublin, August 2006, pages 224-229.
- P. Mosses, J. Power, M. Seisenberger, editors, CALCO-jnr 2005,CALCO Young Researchers Workshop, Swansea, September 2005, Selected papers, University of Wales Swansea Computer Science Report Series CSR 18-2005, 2005
- U. Berger, M. Seisenberger, Applications of inductive definitions and choice principles to program synthesis, In: Laura Crosilla and Peter Schuster, editors, From Sets and Types to Topology and Analysis Towards practicable foundations for constructive mathematics, Oxford Logic Guides, Volume 48, Oxford University Press, 137--148, 2005.
- M. Seisenberger, On the Constructive Content of Proofs, PhD thesis, Ludwig-Maximilians-Universität München, Fakultät für Mathematik, Informatik und Statistik, 2003. Abstract and bib reference, Electronical Publication, LMU.
- M. Seisenberger, An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma. In: P. Callaghan, Z. Luo, J. McKinna, R. Pollack, editors, Types for Proofs and Programs (TYPES'00), LNCS 2277, 2001. ( pdf )
- U. Berger, H. Schwichtenberg, and M. Seisenberger, The Warshall Algorithm and Dickson's Lemma: Two Examples of Realistic Program Extraction, Journal of Automated Reasoning 26, Kluwer Academic Publishers, Dordrecht, 2001.
- M. Seisenberger, Kruskal's tree theorem in a constructive theory of inductive definitions In: P. Schuster, U. Berger, H. Osswald, editors, Reuniting the Antipodes - Constructive and Nonstandard Views of the Continuum. Proceedings of the Symposion in San Servolo/Venice, Italy, May 17-22, 1999. Synthese Library 306, Kluwer Academic Publishers, Dordrecht, 2001, pp. 241-255.
- H. Benl, U. Berger, H. Schwichtenberg, M. Seisenberger and W. Zuber, Proof theory at work: Program development in the Minlog system In: W. Bibel and P.H. Schmitt, editors, Automated Deduction - A Basis for Applications II, Kluwer 1998, pp. 41-71.
