Picture by Will Harwood
at CALCOjnr
Contact:
Dr Monika Seisenberger
Dept. of Computer
Science
College of Science
Swansea
University
Singleton Park
Swansea SA28PP, UK
f: (+44) (0)1792 295708
e: m.seisenberger@swansea.ac.uk
Monika Seisenberger
PhD Munich, Associate Professor at Swansea University
Programme Director Computer Science
Research:
Program extraction; Modelling, Specification & Verification; Verification of Railway Control Systems; Interactive Theorem Proving; Formal methods in Security and Cyberterrorism; Logic & Proof theory, well and better quasiorderings.
I am a member of Swansea's Theoretical Computer Science group and of the Swansea Railway Verification Group. I coorganized the Proof, Complexity, Verification (PCV) Research Seminar (from 20062013) 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.
Research Projects: Correctness by Construction, CORCON,
FP7 Marie Curie International Research Project, PIRSESGA2013612638, Jan 2014 Dec 2017.
This is a project which involves researchers from Japan, Australia, New Zealand, USA, India, Korea, Sweden, Italy, Germany, and UK and specifically supports and offers training for PhD students. Currently in Swansea we have a vacancy for 12 PhD students to participate in the staff exchange. Swansea's contribution to the project is centered around program verification in general and obtaining correct programs specifically in the case of continuous data. If interested please contact Monika Seisenberger.
Swansea Team: Ulrich Berger, Anton Setzer, Jens Blanck, Arnold Beckmann, Monika Seisenberger (Director).  Comput whenable Analysis, COMPUTAL, FP7 Marie Curie International Research Project, PIRSESGA2011294962, Febr 2012 Jan 2016.
 Andrew Lawrence (Program Extraction, Verification of Railway Control Systems)
 Alison Jones (Proof theoretic methods in Natural Language Processing)
 Sulaiman AlShekaili (Analyzing Organizational Networks, Cyberterrorism)
Conferences and workshops I am/was involved in:
 Wellquasiorderings in Computer Science, Dagstuhl seminar, 1722 Jan 2016 (coorganizer)
 Wellquasiorderings: From Theory to Applications, Minisymposium at DMV 2015, 2125 Sept 2015 (coorganizer)
 Continuity, Computatiblity, Constructivity, CCC2015, Munich/Kochel, 1418 Sept 2015 (coorganizer)
 CALCO 2015 (PC member)
 Continuity, Computability, Constructivity, CCC2014, Ljubljana, 813 September 2014 (PC member).
 Classical Logic and Computation 2014, Vienna, 13 July 2014 (PC member)
 Correctness by Construction, CORCON 2014 Workshop, Genua, 2427 March 2014 (Organization Committee Member)
 Coalgebraic Methods in Computer Science, CMCS 2014 Grenoble, 56 April 2014 (PC member)
 CCC2013, 2630 June 2013, Swansea/Gregynog, Wales (PC member, Coorganizer)
 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, 57 September 2011, Swansea (Coorganizer)
 CALCO Young Researchers Workshop, CALCOjnr 2011, 29 August 2011, Winchester (PC chair)
 Program Extraction and Constructive proofs, Workshop in honor of Helmut Schwichtenberg, 2122 August 2010, Brno, Czech Republic (Coorganizer)
 BCSWomen Lovelace Colloquium 2010 8 April 2010, Cardiff (PC member)
 4th Wessex Theory Seminar Meeting, 29 October 2009, Swansea (Organizer)
 British Logic Colloquium 2009, 35 September 2009, Swansea (Coorganizer)
 CALCO Young Researchers Workshop, CALCOjnr 2009, 6 September 2009, Udine, Italy (PC member)
 3rd Wessex Theory Seminar Meeting, 3 March 2009, Bath, and 4 March 2009, Swansea (Coorganizer)
 Proof, Computation, Complexity, PCC 2008, 89 August 2008, Oslo (PC member)
 Formalising Mathematics and Extracting Algorithms from proofs, CiE2008, 1520 June 2008, Athens (Special session organizer)
 Russell'08, Proof Theory meets Type Theory,1516 March 2008, Swansea (Coorganizer)
 CALCO Young Researchers Workshop, CALCOjnr 2007, 20 August 2007, Bergen (PC member)
 Proof, Computation, Complexity, PCC 2007, 1314 April 2007, Swansea (Coorganizer) Proof theorists on the beach, further photographs from PCC 2007.
 Computability in Europe, CiE 2006, 30 June  5 July 2006, Swansea (Coorganizer) conference photo.
 CALCO Young Researchers Workshop, CALCOjnr 2005, 2 September 2005, Swansea, (PC member, Coorganizer) Day0, CALCOjnr talks, beach party, excursion, all photographs (by Will Harwood).
Industrial Collaboration:
 Siemens Rail Automation, Chippenham, UK,

Academic partner of Esterel Technologies, the provider of modelbased solutions for DO178B and IEC 61508 safetycritical systems.
Teaching:
 CS081 Introduction to Alogrithms and Data Structures, 2014/15 (In Python)
 CS205 Declarative Programming, 20122015 (In Haskell and Prolog)
 CS081 Introduction to Computing II, 2013/14 (Programming in Python)
 CS161 Introduction to Computing I, 20052011, 2012/13
 CS071 / CS171 Introduction to Computing II, 20062011, (in Java)
 CS141 Programming  Principles and Practice 20102011 (in Java)
 CS318 Cryptography and ITSecurity/ CSM18 ITSecurity: Theory and Practice, 20052009
 CS313 High Integrity Systems/ CSM13 Critical Systems, 20062008 (in Spark Ada)
 CS332 Designing Algorithms/ CSM32 Algorithm Design and Analysis, 20042008
 CS151 Introduction to Computing, 2004/2005 (in Java)
 CS226 Computability theory, 2004/2005
 CS213 System Specification, 20042011 (in Maude)
Please find more detailed information, course material, and grades on Blackboard.
Teaching/Administration/ 3rd Mission:
 Programme Director in Computer Science
 Head of Yr 2 (until 31/12/2014)
 The Yr 2 Induction lecture 2014
 Yr 2 tutorial allocation will be announced on Monday 29 September. Tutorials start on 29 September 2014 and take place fortnightly.
 Outreach: Women In Science at Swansea University, SwanSTEMWoMen
 BCS Women in Wales Committee member
 Examination officer (examination papers), 2004July 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
 Member of the Special Circumstances Committee and the Learning and Teaching Committee, 2005July 2011
Refereed Journal and Conference Publications, Invited Publications, PhDthesis, Edited Proceedings:
 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, Andrew Lawrence, Fredrik Nordvall Forsberg, and Monika Seisenberger, Extracting verified decision procedures: DPLL and Resolution, Logical Methods in Computer Science, 2015
 Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods, Extracting Imperative Programs from Proofs: Inplace 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. 84106, 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 9783319050317, 2014. doi:10.1007/9783319050324 19, URL http: //dx.doi.org/10.1007/9783319050324_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 FMRAILBOK 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. 243256, dx.doi.org/10.1016/j.entcs.2012.08.016
 C. Cirstea, M. Seisenberger, T. Wilkinson (editors), CALCO Young Researchers Workshop, CALCOjnr 2011, Selected Papers, Eprint 336337, University of Southampton, 2012.
 U. Berger, M. Seisenberger, Proofs, Programs, Processes, Theory of Computing, Volume 51, Number 3 (2012), 313329 (Journal version, 17 pages), Doi:10.1007/s0022401193258
 U.Berger, K. Miyamoto, H. Schwichtenberg, M. Seisenberger, Minlog  A Tool for Program Extraction for Supporting Algebra and Coalgebra, CALCOTools 2011, LNCS 6859, pp. 393399, 2011. Doi:10.1007/9783642229442_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. 3948, 2010, Doi: 10.1007/9783642139628_5 (conference version, 10 pages)
 M. Haveraaen, M. Lenisa, J. Power, M.Seisenberger, editors, CALCO Young Researchers Workshop, CALCOjnr 2009, Selected papers, Udine, September 2009, Report no 52010, 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, 163167 (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/13, pp 97110, 2008.
 M. Haveraaen, J. Power, M. Seisenberger, editors, CALCO Young Researchers Workshop, CALCOjnr 2007, Selected papers, Bergen, August 2007, University of Bergen, UIB report no 2008367, 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. ShinnerKennedy, 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 153158.
 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. ShinnerKennedy, 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 224229.
 P. Mosses, J. Power, M. Seisenberger, editors, CALCOjnr 2005,CALCO Young Researchers Workshop, Swansea, September 2005, Selected papers, University of Wales Swansea Computer Science Report Series CSR 182005, 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, 137148, 2005.
 M. Seisenberger, On the Constructive Content of Proofs, PhD thesis, LudwigMaximiliansUniversitä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 NashWilliams' MinimalBadSequence 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 1722, 1999. Synthese Library 306, Kluwer Academic Publishers, Dordrecht, 2001, pp. 241255.
 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. 4171.