Monika Seisenberger, Swansea University, UK

Picture by Will Harwood
at CALCO-jnr

Contact:

Dr Monika Seisenberger
Dept. of Computer Science
College of Science
Swansea University
Singleton Park
Swansea SA28PP, UK

t: (+44) (0)1792 602131
f: (+44) (0)1792 295708
e: m.seisenberger@swansea.ac.uk

Monika Seisenberger

PhD Munich, Lecturer at Swansea University

Research:

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.

Conferences and workshops I am/was involved in:

CCC2013, 26-30.June 2013, Swanesa/Gregynog, Wales (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:

Invensys Rail, Chippenham, UK,
Academic partner of Esterel Technologies, the provider of model-based solutions for DO-178B and IEC 61508 safety-critical systems.

From 2006-2011, I coordinated the Proof, Complexity, Verification (PCV) Research Seminar. 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.

Teaching:

CS-061 Introduction to Computing I, 2012-2013
CS-205 Declarative Programming, 2012-2013

CS-061 / 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:

Level 2 Year Head
- Level 2 Induction lecture,28.09.2012
- Level 2 Tutorial Allocation, 03.10.2012, Tutorials start on 8 Oct 2012 and take place fortnightly.

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

Publications:

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 (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), 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
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, 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.
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.