Functional Geekery Episode 62 – Lars Hupel

In this episode I talk with Lars Hupel. We talk his introduction to Functional Programming with Haskell, Scala, and move to working on Isabelle for creating theorems about proving your program.

Our Guest, Lars Hupel

@larsr_h on Twitter
Lars online


Compose Melbourne is a new functional programming conference focused on developing the community and bringing typed functional programming to a wider audience. Visit to find out more.

ElixirConf is taking place August 31st through September 2nd in Orlando, Florida. Visit to register and find out more.

Full Stack Fest will be hold in Barcelona on September 5-9th. You can check out to find out more.

PWLConf 2016 is the first full-day Papers We Love conference, co-located with the preconference events at Strange Loop in Saint Louis, Missouri on September 15th. Keep an eye out for updates on

The Erlang User Conference is coming up in Stockholm, Sweden, the 6th through the 16th of September. Early Bird tickets are now available and get a 10% discount on the conference when you use the code: FunctionalGeekery10 when registering.

Lambda World will be taking place September 30th & October 1st, 2016. Lambda.World is the longest functional programming conference in Spain and Portugal and one of the biggest in Europe. Visit to find out more and to register.

The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit for more information and to register.

CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit to register and submit your talk.

Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit to find out more.

If you have a conference related to functional programming, contact me, and I will be happy to announce it.


About Lars
How Lars
Lars’ first exposure to Haskell from a C and Java background
Using Scala as a transition strategy from OOP to FP
Importance of feedback on actual code
Programming in Scala
Writing the Travelling Sales Person problem in Haskell
Progression to tooling that assures your program is right
Lack of debugger in Haskell and Scala
Use of the REPL in Haskell and Scala
Relation of QuickCheck and ScalaCheck to Isabelle
What is Isabelle
Ability to extract code from Isabelle
HOL higher order logic
Where Isabelle fits with other theorem proving languages
HOL Light
What Lars is working on in Isabelle
Code generation to x86 machine language
Different proving strategies available in Isabelle
Interactive Theorem Proving
Automated Theorem Proving
Relationship between Tactics and Lemmas
Programming and Proving Isabelle
Archive of Formal Proofs
Gödel’s ontological proof
Lambda World
ITP 2016
Check out Isabelle to know what is possible

As always, a giant Thank You goes to David Belcher for the logo design.

Leave a Reply

Your email address will not be published. Required fields are marked *