#30 Actors, GADTs and Burnout
May 30th 2023
Dan and Pedro
#29 Can PL theory make you a better software engineer?
April 9th 2023
Jimmy Koppel
#28 Formally Verifying Smart Contracts
February 15th 2023
Pruvendo
#27 Formalizing an OS: The seL4
February 4th 2023
Gerwin Klein
#26 Mechanizing Modern Mathematics
January 16th 2023
Kevin Buzzard
#25 Formally Verifying the Tezos Codebase
November 21st 2022
Formal Land
#24 The History of Isabelle
October 6th 2022
Lawrence Paulson
#23 What is the SIGPLAN?
September 23th 2022
Jens Palsberg and Jonathan Aldrich
#22 Impredicativity, LEM, Realizability and more
August 12th 2022
Cody Roux
#21 Denotational Design
August 4th 2022
Conal Elliott
#20 Huaweii, String Diagrams, Game Semantics
June 27th 2022
Dan R. Ghica
#19 Experience Report: Learning Coq
June 4th 2022
Patrick and Supun
#18 Gödel's Incompleteness Theorems
May 19th 2022
Cody Roux
#17 The Lost Elegance of Computation
May 9th 2022
Conal Elliott
In this episode I had the pleasure to have an in-depth conversation with Conal Elliott about his life, his work, his philosophy and his many opinions about research and the current state of PL Research and how it lead him to come with the concept of Denotational Design. Conal got his PhD at CMU in the 90s under Frank Pfenning working on Higher-Order Unification, after that he has devoted his life on thinking and refining graphic computation and the tools behind it.
Links
- Conal’s website
- Play/work with Conal
- Conal’s twitter: @conal
- The simple essence of automatic differentiation
- Compiling to categories
- Generic parallel functional programming
- Denotational design with type class morphisms
- Functional Images
- Functional Reactive Animation
- Alphabet Versus the Goddess - Leonard Shlain
- The information - James Gleick
- Murray Gell-Mann’s definition of beauty/elegance: “A theory appears beautiful or elegant […] when it’s simple; in other words when it can be expressed very concisely in terms of mathematics that we’ve already learned for some other reasons.”
- A John Backus quote (from his Turing Award lecture): “Many creative computer scientists have retreated from inventing languages to inventing tools for describing them. Unfortunately, they have been largely content to apply their elegant new tools to studying the warts and moles of existing languages. After examining the appalling type structure of conventional languages, using the elegant tools developed by Dana Scott, it is surprising that so many of us remain passively content with that structure instead of energetically searching for new ones.”
Tweet