LEAN4 is a theorem prover plus dependently typed programming language. In this talk, I describe the compilation pipeline of LEAN4, starting from the high-level abstract syntax tree, to its custom intermediate representation called lambdapure, the optimization passes that are run on lambdapure. and finally its code generation via C.

In the process, we'll learn about lambdapure's interesting properties, such as its optimized reference counting for purely functional programs (https://arxiv.org/pdf/1908.05647.pdf), and the precise details of the runtime code generation into C.

If time permits, I explain my current PhD research, which is modifying LEAN's compilation pipeline to use the new MLIR compilation framework: https://github.com/bollu/lz

I explain the ingredients necessary to implement a minimal dependently typed language (https://github.com/bollu/minitt). I'll explain the ideas of normalization by evaluation on untyped lambda calculus, bidirectional type checking on simply typed lambda calculus, and then scale these up to a full, minimal dependently typed language, dubbed "mini-TT". At the end of the talk, you'll be fully equipped to implement a dependently typed language, and follow along other material such as "The little typer" for a deeper dive. 

We take a dive into probabilistic programming, beginning with a high-level explanation of what probabilistic programming is. We then continue to see how to use the monad-bayes library for performing tasks such as regression in a bayesian formalism. We also look into the implementation of the library, which involves performing an interesting sampling method (markov-chain-monte-carlo) on a very unique space (the space of computational traces of the program). We finally end with next-steps for the haskell community to improve in the probablistic programming space, ala pyro for python

Here is our tiny re-implementation of monad-bayes, boiled down to the essentials: https://github.com/bollu/shakuni

Paper on which the talk is based on: http://mlg.eng.cam.ac.uk/pub/pdf/SciGhaGor15.pdf