Lars-Henrik Eriksson
Senior Lecturer/Associate Professor at Department of Information Technology; Division of Computing Science
- Telephone:
- +46 18 471 10 57
- E-mail:
- Lars-Henrik.Eriksson@it.uu.se
- Visiting address:
- Hus 10, Regementsvägen 10
- Postal address:
- Box 337
751 05 UPPSALA
Short presentation
I teach programming and theory of programming language. I am also Distinguish University Teacher, pedagogical mentor and programme coordinator for the Master Programme in Computer Science.
My research interest is within application of logic to computer science -- particularly the use of formal methods for software development.
Keywords
- programming languages
- programmeringsspråk
- formal methods
- formella metoder
- logik i datavetenskap
- logic in computer science
- datalogi
- computer science
- computing science
- datavetenskap
- programmering
- programming
Biography
DISTINGUISHED UNIVERSITY TEACHER and MENTOR
I am a Distinguished University Teacher and also a pedagogical mentor, that is a member of the university Collegium of Mentors. I teach Computing Science on both basic and advanced levels. The forms of teaching I use the most are projects, seminars, labs and lectures. I also review undergraduate theses.
I am a pedagogical mentor because I feel that teaching -- meeting the students -- is enjoyable and discussing teaching with colleagues is almost even more fun.
TEACHING
Courses I currently teach:
- Advanced Functional Programming
- Imperative and Object-Oriented Programming Methodology
Courses I have previously taught:
- Basic Programming with Didactic Specialisation for Teachers
- Functional Programming
- Provably Correct Software
- Program Design (Programming Methodology 1)
- Program Design and Data Structures
- Programming Methodology 2
- Semantics of Programming Languages
- Software Engineering
- Software Engineering Project
RESEARCH
Refer to a separate section for information about my research.
MANAGEMENT
From 2004 to 2018 I was the Head of the Division of Computing Science of the Department of Information Technology. From 2020 on I am the Programme Coordinator for the Master Programme in Computer Science.
INDUSTRY
Before I had my position at Uppsala University, I worked eight years as a consultant and still do occasional consultancy projects. I have primarily worked with risk analysis and applications of formal methods to railway signalling. I have semiprofessional competence in railway signalling. Among other things I have worked with a project within the Swedish Transport Administration about risk analysis for the implementation of ETCS/ERTMS in Sweden.
I am a partner in Nya Industrilogik SW AB. I was co-founder, board member and technical advisor to Industrilogik L4i AB -- today merged with Prover Technology AB.
MISCELLANEOUS
I have a Private Pilot License with Instrument Rating (PPL/IR). My total flight time is about 1200 hours. I am also the chairman of the (powered) flying club in Uppsala, Motorflygarna Uppsala Flygklubb and teach ground school for the Private Pilot License.
In my spare time I also design, build and maintain relay-based signalling systems for the preserved railroad Uppsala-Lenna Järnväg. I am also a traffic controller for that railway.
Research
My research interests include the use of logic in Computer Science. I have worked with theory and implementation of Logic Programming, Interactive Theorem Proving, Logical Frameworks and Formal Methods (Specification, Verification and Synthesis). I have also done work on methodology for the application of Formal Methods.
Most recently, my work has been on the use of application domain theories in formal methods and on formalising proofs within concurrency theory using Isabelle.
For more information on our research in these areas, refer to https://www.uu.se/en/department/information-technology/research/semantics-and-verification and https://www.uu.se/en/department/information-technology/research/software-engineering.
I am a board member of Formal Methods Europe and was Programme Committee Co-Chair for the FME symposium 2002 (part of FLoC'02).

Publications
Selection of publications
-
Teachers' conceptions of the role of mathematics in STEM higher education
Part of Disciplinary and Interdisciplinary Science Education Research (DISER), 2025
- DOI for Teachers' conceptions of the role of mathematics in STEM higher education
- Download full text (pdf) of Teachers' conceptions of the role of mathematics in STEM higher education
-
Modal Logics for Nominal Transition Systems
Part of Logical Methods in Computer Science, 2021
- DOI for Modal Logics for Nominal Transition Systems
- Download full text 1 (pdf) of Modal Logics for Nominal Transition Systems
- Download full text 2 (pdf) of Modal Logics for Nominal Transition Systems
-
Part of Formal Techniques for Distributed Objects, Components, and Systems, p. 179-193, 2017
-
Part of Electronic Notes in Theoretical Computer Science, p. 77-91, 2007
-
Verification and generation of geographical data using domain theory
Part of TRain Workshop at the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM’05), 2005, 2005
-
Using Formal Methods in a Retrospective Safety Case
Part of Computer Safety, Reliability, and Security, p. 31-44, 2004
-
Specifying railway interlocking requirements for practical use
Part of SAFECOMP'96 – Proceedings of the 15th International Conference on Computer Safety, reliability and Security (SAFECOMP'96), p. 243-249, 1996
-
Finitary partial inductive definitions as a general logic
Part of Extensions of Logic Programming, 4th International Workshop, p. 94-119, 1994
-
Pi: An interactive derivation editor for the calculus of partial inductive definitions
Part of CADE-12 – 12th International Conference on Automated Deduction, Proceedings, p. 821-825, 1994
-
A finitary version of the calculus of partial inductive definitions
Part of Extensions of Logic Programming, p. 89-134, 1992
-
The programming language GCLA – a definitional approach to logic programming
Part of New generation computing, p. 381-404, 1990
-
Synthesis of a unification algorithm in a logic programming calculus
Part of The journal of logic programming, p. 3-18, 1984
Recent publications
-
Teachers' conceptions of the role of mathematics in STEM higher education
Part of Disciplinary and Interdisciplinary Science Education Research (DISER), 2025
- DOI for Teachers' conceptions of the role of mathematics in STEM higher education
- Download full text (pdf) of Teachers' conceptions of the role of mathematics in STEM higher education
-
Modal Logics for Nominal Transition Systems
Part of Logical Methods in Computer Science, 2021
- DOI for Modal Logics for Nominal Transition Systems
- Download full text 1 (pdf) of Modal Logics for Nominal Transition Systems
- Download full text 2 (pdf) of Modal Logics for Nominal Transition Systems
-
Part of Formal Techniques for Distributed Objects, Components, and Systems, p. 179-193, 2017
-
Modal Logics for Nominal Transition Systems
Part of Archive of Formal Proofs, 2016
-
Modal Logics for Nominal Transition Systems
Part of 26th International Conference on Concurrency Theory, p. 198-211, 2015
All publications
Articles in journal
-
Teachers' conceptions of the role of mathematics in STEM higher education
Part of Disciplinary and Interdisciplinary Science Education Research (DISER), 2025
- DOI for Teachers' conceptions of the role of mathematics in STEM higher education
- Download full text (pdf) of Teachers' conceptions of the role of mathematics in STEM higher education
-
Modal Logics for Nominal Transition Systems
Part of Logical Methods in Computer Science, 2021
- DOI for Modal Logics for Nominal Transition Systems
- Download full text 1 (pdf) of Modal Logics for Nominal Transition Systems
- Download full text 2 (pdf) of Modal Logics for Nominal Transition Systems
-
Modal Logics for Nominal Transition Systems
Part of Archive of Formal Proofs, 2016
-
Part of Electronic Notes in Theoretical Computer Science, p. 77-91, 2007
-
Spezifikation von Stellwerkslogik mit formalen Methoden
Part of Signal + Draht, 2004
-
Special Issue: ICLP'94. Preface
Part of Computer languages, 1997
-
The programming language GCLA – a definitional approach to logic programming
Part of New generation computing, p. 381-404, 1990
-
Synthesis of a unification algorithm in a logic programming calculus
Part of The journal of logic programming, p. 3-18, 1984
Conference papers
-
Part of Formal Techniques for Distributed Objects, Components, and Systems, p. 179-193, 2017
-
Modal Logics for Nominal Transition Systems
Part of 26th International Conference on Concurrency Theory, p. 198-211, 2015
-
Verification and generation of geographical data using domain theory
Part of TRain Workshop at the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM’05), 2005, 2005
-
Using Formal Methods in a Retrospective Safety Case
Part of Computer Safety, Reliability, and Security, p. 31-44, 2004
-
Adtranz Signal's Formal Verification Process (2): The STERNOL Specification Tool (SST)
Part of The fourth FMERail Workshop, 1999
-
Some Technical Aspects of an Interlocking Specification language
Part of The fourth FMERail Workshop, 1999
-
An Interlocking Specification Language
Part of Proc. ASPECT'99 Conference, 1999
-
Using formal methods for quality assurance of interlocking systems
Part of WIT Transactions on The Built Environment 37, 1998
-
Specifying railway interlocking requirements for practical use
Part of SAFECOMP'96 – Proceedings of the 15th International Conference on Computer Safety, reliability and Security (SAFECOMP'96), p. 243-249, 1996
-
Verification of Safety-Critical Systems using Fast Automated Theorem Proving
Part of Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT'96, 1996
-
Finitary partial inductive definitions as a general logic
Part of Extensions of Logic Programming, 4th International Workshop, p. 94-119, 1994
-
Pi: An interactive derivation editor for the calculus of partial inductive definitions
Part of CADE-12 – 12th International Conference on Automated Deduction, Proceedings, p. 821-825, 1994
-
A finitary version of the calculus of partial inductive definitions
Part of Extensions of Logic Programming, p. 89-134, 1992
-
A survey of GCLA: a definitional approach to logic programming
Part of Extensions of Logic Programming, p. 49-99, 1991
-
The GCLA II programming language
Part of Processing Declarative Knowledge, PDK'91, p. 399-401, 1991
-
Generalised Horn Clauses as a Programming Language
Part of Proceedings of the Second Scandinavian Conference on Artificial Intelligence, 1989
-
Incorporating mutable arrays into logic programming
Part of Proc. Second International Conference on Logic Programming, p. 76-82, 1984