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
Announcements
Compose Melbourne is a new functional programming conference focused on developing the community and bringing typed functional programming to a wider audience. Visit www.composeconference.org/ to find out more.
ElixirConf is taking place August 31st through September 2nd in Orlando, Florida. Visit http://www.elixirconf.com to register and find out more.
Full Stack Fest will be hold in Barcelona on September 5-9th. You can check out 2016.fullstackfest.com 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 pwlconf.org.
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 www.lambda.world 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 http://scala.io/ 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 codemesh.io to register and submit your talk.
Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more.
If you have a conference related to functional programming, contact me, and I will be happy to announce it.
Topics
About Lars
How Lars
Isabelle
Haskell
Scala
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
scalaz
Relation of QuickCheck and ScalaCheck to Isabelle
What is Isabelle
Ability to extract code from Isabelle
Isar
HOL higher order logic
Where Isabelle fits with other theorem proving languages
Coq
HOL Light
Agda
Idris
What Lars is working on in Isabelle
Code generation to x86 machine language
Lem
Different proving strategies available in Isabelle
Interactive Theorem Proving
Automated Theorem Proving
Tactics
Lemmas
Relationship between Tactics and Lemmas
Programming and Proving Isabelle
Archive of Formal Proofs
Gödel’s ontological proof
Typelevel
Lambda World
ITP 2016
EPFL
Check out Isabelle to know what is possible
As always, a giant Thank You goes to David Belcher for the logo design.