Picture by Will Harwood
Dr Monika Seisenberger
Dept. of Computer Science
College of Science
Swansea SA28PP, UK
f: (+44) (0)1792 295708
PhD Munich, Senior Lecturer at Swansea University
Formal methods: Program extraction, interactive theorem proving, specification and verification. Logic: proof theory, infinitary combinatorics, in particular well- and better quasiorderings.
I am a member of Swansea's theory group Logic and Computation and of the Swansea Railway Verification Group. Since 2006, I co-organize the Proof, Complexity, Verification (PCV) Research Seminar and I am the Swansea site leader in the Wessex Theory Seminar, a Joint Seminar Series of Mathematics and Computer Science Departments, and Industrial Collaborators, broadly in the Wessex region.x
Conferences and workshops I am/was involved in:
- 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).
- Invensys Rail, Chippenham, UK,
- Andrew Lawrence
- Alison Jones
- Sulaiman Al-Shekaili
- CS-081 Introduction to Computing II, 2013-2014 (In Python, Programming, Problem Solving, Algorithms and Data Structures)
- CS-205 Declarative Programming, 2012-2013, 2013-2014 (In Prolog/Haskell)
- CS-061 Introduction to Computing I, 2012-2013 (Programming in Java)
- CS-161 Introduction to Computing I, 2005-2011
- CS-071 / CS-171 Introduction to Computing II, 2006-2011
- CS-141 Programming - Principles and Practice, 2010-2011
- 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
- CS-332 Designing Algorithms/ CS-M32 Algorithm Design and Analysis, 2004-2008
- CS-151 Introduction to Computing, 2004/2005
- CS-226 Computability theory, 2004/2005
- CS-213 System Specification, 2004-2011
Please find more detailed information, course material, and grades on Blackboard.
Administration/ 3rd Mission:
- Level 2 Year Head
- The Level2 Induction lecture (slides) can be found on Blackboard.
- Level 2 Tutorial Allocation, 04.10.2013, Tutorials start on 7 Oct 2013 and take place fortnightly.
- Computer Science Board of Studies member
- SwanseaScienceGrrl Co-lead, see also WomenInScience@SwanseaUniversity
- BCS Women in Wales Committee member
- 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
- Organiser of Student Enrolment, 2006- July 2011
- Head of Foundation Year, 2008- July 2011
- Member of the Special Circumstances Committee and the Learning and Teaching Committee, 2005-July 2011
- 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.