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, Lägerhyddsvägen 1
- Postadress:
- Box 337
751 05 UPPSALA
- Akademiska meriter:
- FD, Excellent lärare
Mer information visas för dig som medarbetare om du loggar in.
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. För mer information om vår forskning inom dessa områden, se https://www.it.uu.se/research/semantics-and-verification och https://www.it.uu.se/research/SE.
Nyckelord
- computer science
- computing science
- datalogi
- datavetenskap
- formal methods
- formella metoder
- logic in computer science
- logik i datavetenskap
- programmering
- programmeringsspråk
- programming
- programming languages
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 1000 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.it.uu.se/research/semantics-and-verification och https://www.it.uu.se/research/SE.
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 (2021)
- Weak Nominal Modal Logic (2017)
- Modal Logics for Nominal Transition Systems (2015)
- The GTO Toolset and Method (2007)
- Verification and generation of geographical data using domain theory (2005)
- Using Formal Methods in a Retrospective Safety Case (2004)
- FME 2002: Formal Methods - Getting IT Right : International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002. Proceedings (2002)
- Special Issue: ICLP'94. Preface (1997)
- Specifying railway interlocking requirements for practical use (1996)
- Pi: An interactive derivation editor for the calculus of partial inductive definitions (1994)
- Finitary partial inductive definitions as a general logic (1994)
- A finitary version of the calculus of partial inductive definitions (1992)
- Extensions of Logic Programming Second International Workshop, ELP’91 Stockholm, Sweden, January 27–29, 1991 Proceedings (1992)
- The programming language GCLA – a definitional approach to logic programming (1990)
- Synthesis of a unification algorithm in a logic programming calculus (1984)
- Incorporating mutable arrays into logic programming (1984)
Senaste publikationer
- Modal Logics for Nominal Transition Systems (2021)
- Weak Nominal Modal Logic (2017)
- Modal Logics for Nominal Transition Systems (2016)
- Modal Logics for Nominal Transition Systems (2015)
- The GTO Toolset and Method (2007)
Alla publikationer
Artiklar
- Modal Logics for Nominal Transition Systems (2021)
- Modal Logics for Nominal Transition Systems (2016)
- The GTO Toolset and Method (2007)
- Spezifikation von Stellwerkslogik mit formalen Methoden (2004)
- Special Issue: ICLP'94. Preface (1997)
- The programming language GCLA – a definitional approach to logic programming (1990)
- Synthesis of a unification algorithm in a logic programming calculus (1984)
Böcker
- FME 2002: Formal Methods - Getting IT Right : International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002. Proceedings (2002)
- Finitary Partial Inductive Definitions and General Logic (1993)
- Extensions of Logic Programming Second International Workshop, ELP’91 Stockholm, Sweden, January 27–29, 1991 Proceedings (1992)
Konferenser
- Weak Nominal Modal Logic (2017)
- Modal Logics for Nominal Transition Systems (2015)
- Verification and generation of geographical data using domain theory (2005)
- Using Formal Methods in a Retrospective Safety Case (2004)
- Some Technical Aspects of an Interlocking Specification language (1999)
- Adtranz Signal's Formal Verification Process (2) (1999)
- An Interlocking Specification Language (1999)
- Using formal methods for quality assurance of interlocking systems (1998)
- Verification of Safety-Critical Systems using Fast Automated Theorem Proving (1996)
- Specifying railway interlocking requirements for practical use (1996)
- Pi: An interactive derivation editor for the calculus of partial inductive definitions (1994)
- Finitary partial inductive definitions as a general logic (1994)
- A finitary version of the calculus of partial inductive definitions (1992)
- The GCLA II programming language (1991)
- A survey of GCLA: a definitional approach to logic programming (1991)
- Generalised Horn Clauses as a Programming Language (1989)
- Incorporating mutable arrays into logic programming (1984)
Rapporter
- Use of Domain Theories in Applied Formal Methods (2006)
- A Comparison of Four Propositionakl Theorem Provers (2000)
- Formal Methods Strategy Study Report (2000)
- Formalising railway interlocking requirements (1997)
- Formal verification of railway interlockings (1997)
- Formal specification and validation of a cache-coherence protocol (1995)
- A programming calculus based on partial inductive definitions (with an introduction to the theory of partial inductive definitions) (1988)