Resume

Profile picture

Lars Hupel is a PhD student at TU München in the field of logic and verification. His research focus is on techniques for verified code generation from theorem provers. Additionally, he has worked on formal treatments of Linux firewalls. A frequent conference speaker and co-founder of the Typelevel initiative, he is active in the open source community, particularly in Scala. He also enjoys programming in Haskell, Prolog, and Rust.

Education

PhD Student
since 2013

Technische Universität München, Chair for Logic and Verification

Thesis Working Title: Verification of Code Generators in Isabelle
Master of Science in Informatics
2012–2013

Technische Universität München

Erasmus Exchange Semester
09/2010–01/2011

Queen's University Belfast

Bachelor of Science in Informatics
2008–2012

Technische Universität München

Work

Research Assistant & Teaching Assistant
08/2013–11/2018

Technische Universität München, Chair for Logic and Verification

Research Internship
08/2015–09/2015

École polytechnique fédérale de Lausanne, Lab for Automated Reasoning and Analysis

Student Teaching Assistant
05/2011–10/2011, 05/2012–03/2013

Technische Universität München

Student Teaching Assistant
10/2010–12/2010

Queen's University Belfast

Student Research Assistant
11/2009–07/2010, 12/2011–03/2012

Technische Universität München

Software Engineer
2007–2013

Consultant

Technologies: PHP, Java, Java EE, Scala, MySQL, Play Framework

Select Publications

A Verified Compiler from Isabelle/HOL to CakeML

Lars Hupel ORCID Tobias Nipkow ORCID
European Symposium on Programming (ESOP, Open Access), 2018
The final publication is available at Springer Link.


Verified iptables Firewall Analysis and Verification

Cornelius Diekmann ORCID Lars Hupel ORCID Julius Michaelis Maximilian Haslbeck ORCID Georg Carle ORCID
Journal of Automated Reasoning (Open Access), 2018
The final publication is available at Springer Link.


Translating Scala Programs to Isabelle/HOL

Lars Hupel ORCID Viktor Kunčak
International Joint Conference on Automated Reasoning (IJCAR), 2016
The final publication is available at Springer Link.


Skills

Functional & Logic Programming

Scala (expert), Isabelle, Prolog, Haskell (advanced), OCaml (beginner)

Imperative Programming

Java, C++11, Python (advanced)

Language Ecosystems

Typelevel (cofounder)

IT Operations

Linux administration, LXC, Ansible (advanced)

Software Tooling

Jenkins setup & operations (advanced)

Planning

Open source maintenance, Conference organisation

Languages

German (native), English (fluent), French (basic)

Conference Talks

Numeric Programming with Spire

Scala Italy, 2018


Translating Scala Programs to Isabelle/HOL

International Joint Conference on Automated Reasoning, 2016

Slides Link

How to test proper{t,l}y

flatMap(Oslo), 2016


OptimusPrimeT (cats edition)

Lambda World, 2015


What Haskell can learn from Scala

Haskell eXchange, 2015


When Types are Not Enough

Scala World, 2015


Semantics-Preserving Simplification of Real-World Firewall Rule Sets

Formal Methods, 2015

Slides Link

OptimusPrimeT (cats edition)

flatMap(Oslo), 2015


Functional Mocking

Lambda Days, 2015


State of the Typelevel

Scala eXchange, 2014 (Keynote)


The Next 1100 Haskell Programmers

Haskell Symposium, 2014


Typelevel Scala: What does it mean for the language, the ecosystem, the community, and you?

Scala.IO, 2014

Recording Link

OptimusPrimeT

Scala.IO, 2014


Macros vs Types

Northeast Scala Symposium, 2014


Generating Type Class Instances Automatically

Scala Workshop, 2013

Slides Link

Seven at one blow

Northeast Scala Symposium, 2013