Lean in Lean

• 语言: 英语
• 格式: .pdf
• 来源: lean-lang.org

摘要

Lean in Lean Leonardo de Moura - MSR - USA Workshop Programming Language http://leanprover.github.io Lean • Goals • Extensibility, Expressivity, Scalability, Proof stability • Functional Programming (efficiency) • Platform for • Developing custom automation and domain specific languages (DSLs) • Software verification • Formalized Mathematics • Dependent Type Theory • de Bruijn’s principle: small trusted kernel, external proof/type checkers Programming Language Lean Timeline • Lean 1 (2013) Leo and Soonho Kong • Almost useless • Brave (crazy?) users in 2014: Jeremy Avigad, Cody Roux and Floris van Doorn • Lean 2 (2015) Leo and Soonho Kong • First official release • Emacs interface • Floris van Doorn develops the HoTT library for Lean • First Math library (Jeremy Avigad, Rob Lewis, and many others) • Lean 3 (2016) Leo, Daniel Selsam, Gabriel Ebner, Jared Roesch, Sebastian Ullrich • Lean is now a programming language (interpreter) • Metaprogramming and White box automation • VS Code interface • Lean 4 (202x) Leo and Sebastian Ullrich • Lean In Lean • Compiler Metaprogramming • Extend Lean using Lean • Proof/Program synthesis • Access Lean internals using Lean • Type inference • Unifier • Simplifier • Decision procedures • Type class resolution • … White box automation APIs (in Lean) for accessing data-structures and procedures found in SMT solvers and ATPs. Dependent Type Theory • Before we started Lean, we have studied different theorem provers: ACL2, Agda, Automath, Coq, HOL, HOL Light, Isabelle, Mizar, PVS. • Dependent Type Theory is really beautiful. • Some advantages: • Builtin computational interpretation. • Same data structure for representing proofs and terms. • Reduce code duplication: • Compiler for Haskell-like recursive equations, we can use it to write proofs. • Mathematical structures (e.g., Groups and Rings) are first-class citizens. • Some references: • In praise of dependent types (Mike Shulman) • Typ...