ZARZA We are Zarza, the prestigious firm behind major projects in information technology.

More on Lean

Iowa Type Theory Commute

12/03/2022 15 min Temporada 3 Episodio 27

Listen "More on Lean"

Descargar episodio

Episode Synopsis

I talk about my positive experience trying out the tools for Lean, specifically the 'lean' executable and lean-mode in emacs.

More episodes of the podcast Iowa Type Theory Commute

Measure Functions and Termination of STLC 14/11/2025

Schematic Affine Recursion, Oh My! 22/08/2025

The Stunner: Linear System T is Diverging! 19/08/2025

Terminating Computation First? 01/08/2025

Correction: the Correct Author of the Proof from Last Episode, and an AI flop 12/05/2025

Krivine's Proof of FD, Using Intersection Types 05/05/2025

A Measure-Based Proof of Finite Developments 16/04/2025

Introduction to the Finite Developments Theorem 27/03/2025

Nominal Isabelle/HOL 31/01/2025

The Locally Nameless Representation 02/01/2025

Ver todos los episodios