Lars-Henrik Eriksson
Universitetslektor vid Institutionen för informationsteknologi; Datalogi
- Telefon:
- 018-471 10 57
- E-post:
- Lars-Henrik.Eriksson@it.uu.se
- Besöksadress:
- Hus 10, Regementsvägen 10
- Postadress:
- Box 337
751 05 UPPSALA
- Akademiska meriter:
- FD, Excellent lärare
Kort presentation
Jag undervisar i programmering och teori för programmeringsspråk. Jag är också excellent lärare, pedagogisk mentor och programansvarig för masterprogrammet i datavetenskap.
Mitt forskningsintresse är inom tillämpningar av logik i datavetenskap -- speciellt formella metoder för programvaruutveckling.
Nyckelord
- programming languages
- programmeringsspråk
- formal methods
- formella metoder
- logik i datavetenskap
- logic in computer science
- datalogi
- computer science
- computing science
- datavetenskap
- programmering
- programming
Biografi
EXCELLENT LÄRARE och MENTOR
Jag är excellent lärare och även pegagogisk mentor, alltså ledamot av mentorskollegiet. Min undervisning är i datalogi både på grundnivå och avancerad nivå, huvudsakligen på programkurser. De pedagogiska undervisningsformer jag använder mest är (projekt)handledning, seminarier, laborationer och föreläsningar. Jag granskar också examensarbeten.
Jag är pedagogisk mentor därför att jag tycker att undervisning, mötet med studenterna, är roligt och diskussion med kolleger om undervisning är nästan ännu roligare.
Jag kan även ge mentorshandledning på engelska.
UNDERVISNING
De kurser jag undervisar i just nu:
- Avancerad Funktionell Programmering
- Imperativ och objektorienterad programmeringsmetodik
De kurser jag har undervisat i:
- Bevisbart korrekt programvara
- Grundläggande programmering med didaktisk inriktning för lärare
- Funktionell programmering
- Programkonstruktion (Programmeringsmetodik 1)
- Programkonstruktion och datastrukturer
- Programmeringsmetodik 2
- Programvaruteknik
- Projekt i mjukvaruutveckling
- Semantik för programmeringsspråk
FORSKNING
Se separat avsnitt för information om min forskning.
LEDNINGSUPPDRAG
Från 2004 till 2018 var jag avdelningsföreståndare för avdelningen för datalogi vid Institutionen för informationsteknologi. Från och med 2020 är jag programansvarig för masterprogrammet i datavetenskap.
INDUSTRI
Innan jag började arbeta på Uppsala universitet så arbetade jag åtta år som konsult och gör fortfarande enstaka konsultprojekt. Främst har jag arbetat med riskanalys och tillämpningar av formella metoder inom järnvägssignalering. Jag har halvprofessionell kompetens inom järnvägssignalering. Bl.a. har jag arbetat med ett projekt inom Trafikverket för riskanalys av införandet av ETCS/ERTMS i Sverige.
Jag är delägare i Nya Industrilogik SW AB. Jag var (med)grundare, styrelseledamot och teknisk rådgivare till Industrilogik L4i AB -- numera uppköpt av Prover Technology AB.
ÖVRIGT
Jag har privatflygcertifikat med instrumentflygbehörighet (PPL/IR). Min totala flygtid är c:a 1100 timmar. Jag är också ordförande i Motorflygarna Uppsala Flygklubb och lärare på teoriutbildningen till privatflygarcertifikat.
På fritiden ägnar jag mig också åt att projektera, bygga och underhålla reläbaserade järnvägssignalsystem för museijärnvägen Uppsala-Lenna Järnväg. Jag är också trafikledare där.
Forskning
Mina forskningsintressen omfattar användningen av logik inom datavetenskap. Jag har arbetat med teori och implementering av logikprogrammering, interaktiv teorembevisning, logiska ramverk och formella metoder (specifikation, verifiering och syntes). Jag har även arbetat med metodik kring användning av formella metoder.
Min aktuella forskning handlar om användningen av modeller av tillämpningsområden inom formella metoder och formalisering av bevis inom teori för "concurrency" med hjälp av Isabelle.
För mer information om vår forskning inom dessa områden, se https://www.uu.se/institution/informationsteknologi/forskning/semantik-och-verifiering och https://www.uu.se/institution/informationsteknologi/forskning/programvaruteknik.
Jag är styrelseledamot för Formal Methods Europe och var programkommittéordförande för FME symposium 2002 (del av FLoC'02).

Publikationer
Urval av publikationer
Modal Logics for Nominal Transition Systems
Ingår i Logical Methods in Computer Science, 2021
- DOI för Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 1 (pdf) av Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 2 (pdf) av Modal Logics for Nominal Transition Systems
Ingår i Formal Techniques for Distributed Objects, Components, and Systems, s. 179-193, 2017
Modal Logics for Nominal Transition Systems
Ingår i 26th International Conference on Concurrency Theory, s. 198-211, 2015
Ingår i Electronic Notes in Theoretical Computer Science, s. 77-91, 2007
Verification and generation of geographical data using domain theory
Ingår i 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
Ingår i Computer Safety, Reliability, and Security, s. 31-44, 2004
2002
Special Issue: ICLP'94. Preface
Ingår i Computer languages, 1997
Specifying railway interlocking requirements for practical use
Ingår i SAFECOMP'96 – Proceedings of the 15th International Conference on Computer Safety, reliability and Security (SAFECOMP'96), s. 243-249, 1996
Finitary partial inductive definitions as a general logic
Ingår i Extensions of Logic Programming, 4th International Workshop, s. 94-119, 1994
Pi: An interactive derivation editor for the calculus of partial inductive definitions
Ingår i CADE-12 – 12th International Conference on Automated Deduction, Proceedings, s. 821-825, 1994
1992
A finitary version of the calculus of partial inductive definitions
Ingår i Extensions of Logic Programming, s. 89-134, 1992
The programming language GCLA – a definitional approach to logic programming
Ingår i New generation computing, s. 381-404, 1990
Incorporating mutable arrays into logic programming
Ingår i Proc. Second International Conference on Logic Programming, s. 76-82, 1984
Synthesis of a unification algorithm in a logic programming calculus
Ingår i The journal of logic programming, s. 3-18, 1984
Senaste publikationer
Modal Logics for Nominal Transition Systems
Ingår i Logical Methods in Computer Science, 2021
- DOI för Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 1 (pdf) av Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 2 (pdf) av Modal Logics for Nominal Transition Systems
Ingår i Formal Techniques for Distributed Objects, Components, and Systems, s. 179-193, 2017
Modal Logics for Nominal Transition Systems
Ingår i Archive of Formal Proofs, 2016
Modal Logics for Nominal Transition Systems
Ingår i 26th International Conference on Concurrency Theory, s. 198-211, 2015
Ingår i Electronic Notes in Theoretical Computer Science, s. 77-91, 2007
Alla publikationer
Artiklar i tidskrift
Modal Logics for Nominal Transition Systems
Ingår i Logical Methods in Computer Science, 2021
- DOI för Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 1 (pdf) av Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 2 (pdf) av Modal Logics for Nominal Transition Systems
Modal Logics for Nominal Transition Systems
Ingår i Archive of Formal Proofs, 2016
Ingår i Electronic Notes in Theoretical Computer Science, s. 77-91, 2007
Spezifikation von Stellwerkslogik mit formalen Methoden
Ingår i Signal + Draht, 2004
Special Issue: ICLP'94. Preface
Ingår i Computer languages, 1997
The programming language GCLA – a definitional approach to logic programming
Ingår i New generation computing, s. 381-404, 1990
Synthesis of a unification algorithm in a logic programming calculus
Ingår i The journal of logic programming, s. 3-18, 1984
Doktorsavhandlingar, monografi
Konferensbidrag
Ingår i Formal Techniques for Distributed Objects, Components, and Systems, s. 179-193, 2017
Modal Logics for Nominal Transition Systems
Ingår i 26th International Conference on Concurrency Theory, s. 198-211, 2015
Verification and generation of geographical data using domain theory
Ingår i 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
Ingår i Computer Safety, Reliability, and Security, s. 31-44, 2004
Some Technical Aspects of an Interlocking Specification language
Ingår i The fourth FMERail Workshop, 1999
Adtranz Signal's Formal Verification Process (2): The STERNOL Specification Tool (SST)
Ingår i The fourth FMERail Workshop, 1999
An Interlocking Specification Language
Ingår i Proc. ASPECT'99 Conference, 1999
Using formal methods for quality assurance of interlocking systems
Ingår i WIT Transactions on The Built Environment 37, 1998
Specifying railway interlocking requirements for practical use
Ingår i SAFECOMP'96 – Proceedings of the 15th International Conference on Computer Safety, reliability and Security (SAFECOMP'96), s. 243-249, 1996
Verification of Safety-Critical Systems using Fast Automated Theorem Proving
Ingår i Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT'96, 1996
Finitary partial inductive definitions as a general logic
Ingår i Extensions of Logic Programming, 4th International Workshop, s. 94-119, 1994
Pi: An interactive derivation editor for the calculus of partial inductive definitions
Ingår i CADE-12 – 12th International Conference on Automated Deduction, Proceedings, s. 821-825, 1994
A finitary version of the calculus of partial inductive definitions
Ingår i Extensions of Logic Programming, s. 89-134, 1992
A survey of GCLA: a definitional approach to logic programming
Ingår i Extensions of Logic Programming, s. 49-99, 1991
The GCLA II programming language
Ingår i Processing Declarative Knowledge, PDK'91, s. 399-401, 1991
Generalised Horn Clauses as a Programming Language
Ingår i Proceedings of the Second Scandinavian Conference on Artificial Intelligence, 1989
Incorporating mutable arrays into logic programming
Ingår i Proc. Second International Conference on Logic Programming, s. 76-82, 1984