llya Sergey ilyasergey.net NUS Workshop on Formal Proofs and Lean 22 April 2024
● Associate Professor at NUS School of Computing ● Running VERSE lab (verse-lab.github.io) ● Previously: Assistant Professor at UCL (2015-2018) ● Research Interests: ● Design of Programming Languages ● Computer-Aided Software Verification ● Program Synthesis ● Using proof assistants since 2012 ● Wrote a textbook on Coq/SSreflect (ilyasergey.net/pnp) slıdes of thıs talk 2 Proving as Programming or The Curry-Howard correspondence: a link between Computer Science and Logic based on 2018/19 lectures by Xavier Leroy at Collège de France xavierleroy.org/CdF/2018-2019/
Since its inception, computer science has taken many ideas and many principles from mathematical logic. (Church, Turing, von Neumann, and many other founders of computer science were logicians or had beed trained in logic.) This talk outlines the history of seminal interaction between logic and computer science, and more precisely between proof theory and programming languages. 4
Many programming languages treat programs as formulas of a logic: ●  Logic programming (Prolog, Mercury, ...) ●  Constraint programming (Prolog III, CHIP, Oz, …) ●  Queries in relational databases. Executing the program amounts to proving or refuting the corresponding logical formula.
A Prolog program: append([]，L，L）. append([H|T], L, [H|M]) :- append(T, L, M). ?- append(X, Y, [1,2,3]). These Horn clauses and the final query define a logical formula: (∀L, append([], L, L)) (∀H, T, L, M, append(T, L, M) ⇒ append([H|T], L, [H|M]))ハ↑  ∃X, Y, append(X, Y, [1, 2, 3]) Executing the program amounts to proving this proposition by finding appropriate X, Y that satisfy the ∃.
Logic programming falls within a rather natural correspondence...
This is not the Curry-Howard correspondence.
An isomorphism between an intuitionistic (constructive) logic and the simply-typed λ-calculus (the core of a functional programming language).
Complete change of viewpoint: programs are no longer propositions, but the proofs of propositions. 8
Inspires a new perspective on logics and on programming languages, summarized by the “PAT principle”: Propositions As Types Proofs As Terms
A guiding principle to design, understand, and formalize programming languages (mostly, but not only, functional languages, such as OCaml and Haskell). New ways to program, integrating formal verification (e.g., dependent types). New ways to do mathematics, leveraging the power of the computer. Powerful and versatile tools such as Coq and Lean, to help us explore this border between computer science and mathematics.
●  Towards Curry-Howard: the Lambda-Calculus ●  Intuitionistic Logic and the idea of Constructive Proofs ●  Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair 12
Circa 1930, Alonzo Church introduces the notation λx. e meaning “the function that maps parameter x to expression e”. Today we write x → e. However, this notation, popularized by Bourbaki, was introduced later. These notations λx. e or x → e are useful to clarify the way mathematicians talk about functions… “ the function x² ” X → x² or λx. x² (x, y) → x² + y² or λx.λy. x² + y² “ the function x² + y² " “ the family of functions cx² ” c ↦ (x → cx²) or λc.λx. cx²
13

Two main computation rules: α-conversion: renaming a bound variable. λx. M =α λy. M{x ← y}        if y not free in M β-conversion: replacing the formal parameter by the actual argument in a function body. ( λ x. M)( N ) = β M{x ← N} In ordinary mathematics we write: Consider the function f(x) = x + 1. We have that f(2) = 3. The lambda-notation decomposes this computation in multiple steps: f(2) = (λx.x+1)(2) =β 2+1 = 3
14

Dana Scott tells that he once wrote Church Dear professor Church: why “lambda”? and received the following reply Eeny, meeny, miny, moe. Rosser tells that Church progressively simplified the notation îe that is used in Russell and Whitehead’s Principia Mathematica:
In λx.e, variable x is said to be “bound” and can be renamed without changing the meaning. Bound variables appear in various mathematical notations:
16
A minimalistic formal system to express algorithms as compositions of functions M, N ::= x |  λx. M | M N α-equivalence and β-reduction (= oriented conversion): ( λ x.M) N → β M{x ← N} λx.M =α λy.M{x ← y} (y not free in M) A notion of computation appears: iterate β -reduction until an irreducible “normal form” N is reached. M → β M1 → β M2 → β ... → β N → β 17
Church (1936) shows the first undecidability results (= cannot be computed by a general recursive function): ●  Whether a term M has a normal form is undecidable. ●  Corollary: Hilbert’s decision problem (Entscheidungsproblem) has no solution. Kleene (1935) and Turing (1937) show equivalences between ●  general recursive functions (Herbrand, Gödel, Kleene); ●  functions computable by a Turing machine; ●  functions definable as a λ-term via Church’s encoding of natural numbers (1933):
18
The pure lambda-calculus as the common ancestor and as the kernel of functional programming languages: functional language    =    pure lambda-calculus + reduction strategy + data types + type system (if applicable) LISP 1.5 (1960) refers to Church and writes (LAMBDA  . . . ) for anonymous functions. However, its semantics (dynamic scoping of bindings) does not follow β-reduction. Landin (1965) proposes ISWIM, an extended lambda-calculus, as the basis for The next 700 programming languages. After 1970, all functional languages contain lambda-calculus as a kernel: Common Lisp, Scheme, SML, Caml, Haskell, ... 19
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
●  Towards Curry-Howard: the Lambda-Calculus ●   Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
Intuitionism: a philosophy of mathematics developed by Brouwer (1881–1966). Requires all mathematical objects to be accessible to intuition. Rejects non-constructive proofs. Intuitionistic logic: family of logics studied by Heyting, Glivenko, Gödel, Kolmogorov. Formalizes the “only constructive proofs” aspect of intuitionism.
How to prove “there exists x ∈ A such that P(x)” ? ● Constructively: we define an element a of A from the ●  By contradiction: we assume ∃ x ∈ A. P(x) false, that is, we assume ∀x ∈ A. ¬P(x) true, and we deduce a contradiction. For an intuitionist, the first proof is the only valid way to show that ∃χ ∈ A. P(x) is true. The second proof only shows that ∃ x ∈ A. P(x) is not absurd, which is a weaker result. An intuitionistic adventure (inspired by G. Dowek, Computation, Proof, Machine) In the train back from the Netherlands, someone drops me a note: The French classicist logicians want to kill you. Get off at the last stop before the French border. Note: the train may make extra unplanned stops. At which stop should I get off the train? The set A of all stops outside France is 1- nonempty (Brussels ∈  A), 2- totally ordered, and 3- finite; hence, it contains a maximal element; this is “my” stop. However, this proof is not constructive and fails to give me an effective criterion to decide at each stop whether to get off or stay… Excluded middle The excluded middle principle (tertium non datur, tiers exclu): P V →P  for all proposition P Equivalent to double negation elimination: ¬¬P ⇒ P  for all proposition P This is the principle for proofs by contradiction. Intuitionistic logic rejects excluded middle (and the many equivalent rules).
25
Truth vs provability Classical logic: every proposition is a priori true or false. Mathematical proof establishes which of these two cases apply. Intuitionistic logic: a proposition can be proved; or its negation can be proved; otherwise we do not know anything about the proposition.
Provability is characterized by the existence of a construction of the proposition. ●  There exists a construction of T (“true”). ●  There exists no construction of ⊥ (“false”). ●  A construction of P 1 ∧ P 2 is a pair (c 1 , c 2 ) where c₁ is a construction of P₁ and c₂ a construction of P₂. ●  A construction of P 1 V P 2 is a pair (i,c) where i ∈ {1,2} and c is a construction of P i .
Provability is characterized by the existence of a construction of the proposition. ●  A construction of P 1 ⇒ P 2 is a “process” that, given a construction of P1, produces a construction of P2. ●  A construction of ¬P, treated like P ⇒ ⊥, is an algorithm that, from a (hypothetical) construction of P produces a non-existent object. ●  A construction of ∀x, P(x) is an algorithm that, given a value for x, produces a construction of P(x). ●  A construction of ∃ x, P(x) is a pair (α, construction of P(α)).
Let TM be the set of all Turing machines. Consider Q ₫ ∀m ∈ TM,  terminates(m) ∨ ¬terminates(m) Q follows immediately from excluded middle (P V ¬P for all P). Yet, a construction of Q would be an algorithm that, given a Turing machine m, returns (1, c) if m terminates and (2, c) otherwise. Since the halting problem is undecidable, such an algorithm does not exist. Excluded middle is therefore not constructive, since there is no construction that validates it. (This construction would be a universal decision procedure!)
29
A formalization of intuitionistic logic Manipulates intuitionistic sequents of the form Γ ├ P (read: “under hypotheses Г we can deduce Р”.) Comprises axioms (“this sequent is true”) and inference rules (“if the sequents above are true, then the sequent below is true”). For example:
Implication: (“I” stands for Introduction, “E” for Elimination) Г1, Р, Г2 ┣ Р  (Ах) (⇒l) L F P ⇒ Q Г├Р⇒ Q    Г├Р (⇒E, modus ponens) 「下Q Conjunction:
31
Disjunction:
ГトP V Q 「トQ Г ┣ Р V Q
L F P V Q Г, Р ├ R Г, ＱトR (VE) 「トR Negation: 「トP 32
●  Towards Curry-Howard: the Lambda-Calculus ●   Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs ●  Types and Simply-Typed Lambda Calculus ●   Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair Why Types? Folk wisdom: Don’t compare apples to oranges. On n’additionne pas des choux et des carottes. Physical wisdom: dimensional analysis homogeneous, possibly correct d = v.t    dist = dist not homogeneous, always false d = v/t    dist ≠ dist.time-²
To detect and reject some programming errors. (character string ≠ function) "foo"(12) cos(45, "degrees")   (wrong number of arguments) As partial specifications of data structures and module interfaces. type ’a tree = Leaf of ’a | Node of ’a tree * ’a tree val assoc: ’a -> (’a * ’b) list -> ’b To clarify the meaning of programs and facilitate compilation. integer n real x n = n * 2 + 1 (integer arithmetic) (floating-point arithmetic) X = X * 2 + 1 36
In elementary mathematics: an intuitive notion. For example, in Euclidean geometry, a point is not a line, and we never talk about the intersection of two points. In naive set theory: no types a priori. For example, the encoding of natural numbers n + 1 d f n ∪ {n}. But we get paradoxes such as Russell’s: {x | x̸∅ x}. Type theories: add types to a logic to rule out paradoxes. Typing is a sort of superego forbidding certain forms of logical in- cest of the kind x ∈ x. (J.-Y. Girard, The blind spot)
The modern presentation separates the syntax of terms from the typing judgment Г下М : α (read: term M has type α under hypotheses Γ). Terms:   M, N ::= x | λx:α. M | M N Typing rules: Г1, Х : α, Г2 ┣ Х : α Г,х: αトМ : β Гጉλх:α. M : α → β ГトМ : α → β    ГトN : α Г ├ M N : β
Theorem:  (type soundness of simply typed lambda calculus) If  ∅ H M : τ then there exists a value ν = λχ: τ′.N such that M →β*ν . "Well typed programs do not go wrong." – Robin Milner, 1978
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs ●  Types and Simply-Typed Lambda Calculus ●   Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
41

As early as 1930, Curry studies combinatory logic: a variant of the λ-calculus without abstraction λx.Μ, but with combinators predefined by their conversion rules. For example: Terms:   M, N ::= M N | S | K | I Rules: Кху = X S x y z   =  x z (y z) Every λ-term can be encoded in combinatory logic if a suitable combinator basis is provided, such as S, K, I. Typing combinatory logic using simple types: M : α → β    N : α l : α → α K : α → β → α M N : B

42

On pages 313–314 of their book Combinatory logic (1958), Curry and Feys remark that, if we read the arrow in type τ₁ → τ₂ like the implication P ⇒ Q between propositions, ●  The types for the combinators S, K, I are the axioms that define implication in a Hilbert-style logic:
● The typing rule for function application is modus ponens: M : α → β    N : α P ⇒ Q     P M N : B Q
Via Curry’s correspondence, a proposition P is provable if and only if the corresponding type τ is inhabited, that is, there exists a closed term with type τ. Howard's manuscript W. A. Howard, The formulae-as-types notion of construction, 1969 Extends and modernize Curry’s result: ●  Lambda-calculus instead of combinatory logic. ●  Intuitionistic sequents instead of Hilbert-style axioms. ●  Treats the connectors ∧, ∨, → in addition to ⇒; discusses the quantifiers ∀ and ∃. ●  Correspondence between reduction over terms and cut elimination over proofs. Curry-Howard: implication Г1, х : А, Г2トх : А Г, х : АトМ : В Г ├  λ Χ . Μ : Α →  Β Г ├ M : A → B    Г ├ N : A Г ┣ M N : B Curry-Howard: implication Г1, A, Γ 2トA Г, AトB ГトA ⇒ B Гト「トA ⇒ B A ГトB Г is Г without variable names, for example   х : А, у : А — А, А.
Extend the lambda-calculus with pairs and projections: Types:     A, B ::= . . . | A × B Terms:   M, N ::= . . . | 〈M, N〉 | π 1 M | π 2 M Г┣ M : A    Г┣ N : B
Г ┣ M : A × B 48 Curry-Howard: conjunction Extend the lambda-calculus with pairs and projections: Types:     A, B ::= . . . | A × B Terms:   M, N ::= . . . | 〈M, N〉 | π 1 M | π 2 M Гト「トA ∧ B Г上
Extend the lambda-calculus a sum type, its constructors, and pattern matching A, B ::= . . . | A + B Types: Terms:   M,N ::= ... | inj₁ M | inj₂ M match M with inj1 X1 ⇒ N1 | inj2 X2 ⇒ N2 end
Г ├ M : A + B     Г, X 1 : A ├ N 1 : C     Г, X 2 : B ├ N 2 : C Г├ match M with inj₁ X₁ ⇒ N₁ | inj₂ X₂ ⇒ N₂ end : C
50

Extend the lambda-calculus a sum type, its constructors, and pattern matching Types: A, B ::= . . . | A + B Terms:   M,N ::= ... | inj₁ M | inj₂ M match M with inj₁ X₁ ⇒ N₁ | inj₂ X₂ ⇒ N₂ end
「トB
A V B C Г, BトC Гト
Extend the lambda-calculus an empty type and “pattern matching” with zero branches Types:     A, B ::= ... | ⊥ Terms:   M,N ::= ... | match M with end Г ┣ M :工
Extend the lambda-calculus an empty type and “pattern matching” with zero branches Types:     A, B ::= ... | ⊥ Terms:   M,N ::= ... | match M with end ГトT
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
55

Static typing with simple types (as in simply-typed λ-calculus but also as in Algol, Pascal, etc) sometimes forces us to duplicate code.
Example
A sorting algorithm applies to any list list(t) of elements of type t, provided it also receives then function t → t → bool that compares two elements of type t. With simple types, to sort lists of integers and lists of strings, we need two functions with different types, even if they implement the same algorithm: sort_list_int : (int → int → bool) → list(int) → list(int) sort_list_string : (string → string → bool)
There is a tension between static typing on the one hand and reusable implementations of generic algorithms on the other hand. Some languages elect to weaken static typing, e.g. by introducing a universal type “any” or “?” with run-time type checking, or even by turning typing off: void qsort(void * base, size_t nmemb, size_t size, int (*compar)(const void *, const void *)); Instead, polymorphic typing extends the algebra of types and the typing rules so as to give a precise type to a generic function.
57

(John C. Reynolds, Towards a theory of type structure, 1974) We suggest that a solution to [the polymorphic sort function] prob- lem is to permit types themselves to be passed as a special kind of parameter, whose usage is restricted in a way which permits the syntactic checking of type correctness. Extends simply-typed lambda-calculus with the ability to abstract over a type variable and to apply such an abstraction to a type: Terms:   M, N ::= x | λx:t. M | M N
abstraction over type X
Types:
Continuing the list sorting example, the generic sorting function can be given type sort_list : ∀Х. (Х → Х → bool) → list(Х) → list(Х) Its implementation is of the following shape: sort_list = ΛΧ. λcmp : X → X → bool. λl : list(X). M The function can be used for integer lists as well as for string lists just by instantiation: sort_list[int] : (int → int → bool) → list(int) → list(int) sort_list[string] : (string → string → bool)
59

The rules of simply-typed lambda calculus:
Г├ М : t → t'   Г├ N : t
Г ├  λx:t. M : t → t' L H M N : t' Plus two rules for introduction and elimination of polymorphism: Г ├ М : t     Х not free in Г Г ├ М : AX. t Г ┣ ΛΧ. M : ∀Х. t Г ├ M[t'] : t{X ← t'} A new form of β-reduction: (ΛΧ. M)[t] → β   M{X ← t} 60
Second-class polymorphism (~ polymorphic definitions, but monomorphic values): ●  Generics in Ada, Java, C#. ●  Hindley-Milner typing in the ML family languages (SML, OCaml, Haskell, etc), with inference of types, of Λ and of instantiations: for let-bound variables Type scheme:   σ ::= ∀α1, . . . . απ. τ Simple types:   τ ::= α | τ₁ → τ₂ | . . .   for all other variables and values First-class polymorphism (≈ function parameters can have ∀ types): ● Recent extensions of OCaml and of Haskell. An example in OCaml type poly_id = { id : 'a. 'a -> 'a }
61

Simply-typed lambda calculus: Functions: values can be abstracted over values (i.e., values depend on values) Polymorphic lambda calculus: Polymorphic functions: values can be abstracted over types (e.g., polymorphic sorting) Polymorphic lambda calculus with data types: Type constructors: types can be abstracted over types (e.g., List<T> in Java) cf. Barendregt's lambda-cube (1992) What about types depending on values?
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair Ordinary function type A → B bool → nat fun b => match b with
Π(x: A). B(x) N(b: bool). if b then nat else bool fun b => match b with true  =>  0 false => true end
In Fortran, C or C++, the type of an array t [N]  contains ●  a type t: the type of the array elements ●  a “term” (constant expression) N: the size of the array. In other words, the array type constructor takes two parameters, a type t and a term N, and produces the type array(t, N). Lifting the restriction that N is a constant expression, and allowing ourselves to quantify over this N, we can give very precise dependent types to array operations: concat : ∀t.∀N1.∀N2. array(t,N1) → array(t,N2) → array(t,N1 + N2)
Π(x: A). P(x)
Dependent function type corresponds to universal quantification! A familiar dependent type П(Р : nat -> Prop). P(0) ー> (Π(n : nat). P(n) -> P(n.+1)) Π(n : nat). P n ... and its inhabitant in Coq Function nat_ind (P : nat -> Prop) ( f 0  :  P  0 ) (fn : Π(n : nat), P n -> P (n.+1)) := fun (n : nat) => match n with 0 => f0 n'.+1 => fn n' (nat_ind P f0 fn n0) end. 69
Theorem counterexample (A: Type) (P: A → Prop) : (日x: A, ¬P x) → ¬(∀ x, P x). Proof. by case => x H1 H2; apply : H1 (H2 x). Qed.
Theorem counterexample (A: Type) (P: A → Prop) : (日x: A, ¬P x) → ¬(∀ x, P x). Proof. by case => x H1 H2; apply : H1 (H2 x). Qed. Proof term in Coq Function counterexample := fun (A : Type) (P : A -> Prop) (hyp : ∃x : A, ¬ P x) => (fun F : ∀(x : A) (p : (fun x0 : A => ¬ P x0) x), (fun _ : (ﾖx0 : A, ¬ P x0) => ¬ (∀x0 : A, P x0)) (ex_intro (fun x0 : A => ¬ P x0) x p) => match hyp as e return ((fun _ : (∃x : A, ¬ P x) => ¬ (∀x : A, P x)) e) with | ex x x0 => F x x0 end) (fun (x : A) (H1 : ¬ P x) (H2 : ∀x0 : A, P x0) => H1 (H2 x)).
71

theorem counterexample {α: Type} (P: α → Prop) : (∃x: A, ¬P x) → ¬(∀ x, P x) := by sby scase => x H1 H2; apply H1 Proof term in Lean theorem counterexample : ∀ {α : Type} (P : α → Prop), (ﾖx, ¬P x) → ¬A (x : α), P x := fun {{} P H => Exists.casesOn (motive := fun t => H = t → ¬∀ (x : α), P x) H (fun w h h 1 H2 => h (Eq.mp ((congrArg Not ((fun x => eq_true (H2 x)) w)).trans not_true_eq_false) h).elim) (Eq.refl H)
● Scala (limited form) ● Coq/Rocq ● Agda ● Lean theorem reverse_reverse {α : Type} : ∀xs : List α, reverse (reverse xs) = xs          => by rfl X :: XS => by simp [reverse, reverse_append, reverse_reverse xs]
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
75

If propositions = types and proofs = terms, we can reuse principles for proofs construction to generate programs and vice versa. Program  Synthesis Write a theorem specifying a program, build a constructive proof that such program exists, the obtained program is correct by construction. Proof Repair Definitions involved into a theorem changed: Refactor the proof as a program working a new data type to it would type-check, the result is a new valid proof.
76
Program Synthesis (Polikarpova & Sergey, 2019) { X H A * Y H b } void swap(loc x, loc y)
Program Synthesis {x,y}; {xHa*yHb} → {xHb*yHa}  |  ?? Program Synthesis { x, y, a2 } ; { x ↔ a2 * y ↔ b }  ↔ { x ↔ b * y ↔ a2 }  |    ?? (Read) {x,y}; {x↔α*y↔b} → {x↔b*y↔α}  |  let a2 = *x; ??
{ x, y, a2, b2 } ; { x ↔ a2 * y ↔ b2 }    ↔  { x ↔ b2 * y ↔ a2 }    |    ?? (Read) { x, y, a2 }; { x ↦ a2 * y ↦ b }  →  { x ↦ b * y ↔ a2 }  |    let  b2  =  *y;  ?? (Read) {x,y}; {xHa * yHb} → {xHb * yHa}  |  let a2 = *x; ??
{ x, y, a2, b2 } ;  { x ↔ b2  * y ↔ b2 }    { x ↔ b2  * y ↔ a2 }       ?? (Write) { x, y, a2, b2 } ;  { x ↔ a2  *  y ↔ b2 }       { x ↔ b2  *  y ↔ a2 }        *x  =  b2;   ?? (Read) { x, y, a2 }; { x ↦ a2 * y ↦ b }  →  { x ↦ b * y ↔ a2 }  |    let  b2  =  *y;  ?? (Read) {x,y}; {x↔α*y↔b} → {x↔b*y↔α}  |  let a2 = *x; ??
{ x, y, a2, b2 } ;  { y ↔ b2 }  ↔   { y ↔ a2 }  |    ?? • (Frame) { x, y, a2, b2 } ; { x ↦ b2 * y ↔ b2 }   → { x ↔ b2 * y ↔ a2 }   |    ?? - (Write) { x, y, a2, b2 } ;  { x ↔ a2  *  y ↔ b2 }       { x ↔ b2  *  y ↔ a2 }        *x  =  b2;    ?? (Read) { x, y, a2 }; { x ↦ a2 * y ↦ b }  →  { x ↦ b * y ↔ a2 }  |    let  b2  =  *y;  ?? (Read) {x,y}; {x↔α*y↔b} → {x↔b*y↔α}  |  let a2 = *x; ??
{ x, y, a2, b2 } ;  { y ↔ a2 }   →   { y ↔ a2 }   |   ?? (Write) { x, y, a2, b2 } ;  { y ↔ b2 }  ↔  { y ↔ a2 }  |  *y  =  a2;  ?? (Frame) { x, y, a2, b2 } ;  { x ↔ b2  * y ↔ b2 }     { x ↔ b2  * y ↔ a2 }       ?? - (Write) { x, y, a2, b2 } ;  { x ↦ a2  *  y ↔ b2 }       { x ↔ b2  *  y ↔ a2 }        *x  =  b2;    ?? (Read) { x, y, a2 }; { x ↦ a2 * y ↦ b }  →  { x ↦ b * y → a2 }  |    let  b2  =  *y;  ?? {x,y}; {xHa*yHb} → {xHb*yHa}  |  let a2 = *x; ??
{ x, y, a2, b2 } ;  { emp }   →   { emp }  |  ?? (Frame) { x, y, a2, b2 } ;  { y ↔ a2 }   ↔   { y ↔ a2 }   |   ?? (Write) { x, y, a2, b2 } ;  { y ↔ b2 }  ↔  { y ↔ a2 }  |  *y  =  a2;  ?? (Frame) { x, y, a2, b2 } ;  { x ↔ b2  * y ↔ b2 }     { x ↔ b2  * y ↔ a2 }       ?? (Write) { x, y, a2, b2 } ;  { x ↔ a2  * y ↔ b2 }     ↔ b2  * y ↔ a2 }       *x  =  b2;   ?? (Read) { x, y, a2 }; { x ↦ a2 * y ↦ b } → { x ↦ b * y ↔ a2 } |  let  b2  =  *y;  ?? (Read) {x,y}; {x↔α*y↔b} → {x↔b*y↔α}  |  let a2 = *x; ??
(Emp) { x, y, a2, b2 }; { emp }   →   { emp }  |  skip (Frame) { x, y, a2, b2 } ;  { y ↔ a2 }   ↔   { y ↔ a2 }   |   ?? (Write) { x, y, a2, b2 } ; { y ↔ b2 }  ↔ a2 }  | (*y  =  a2;  ?? (Frame) { x, y, a2, b2 } ; { x ↔ b2 * y ↔ b2 }   ↔  { x ↔ b2 * y ↔ a2 }    |    ?? (Write) { x, y, a2, b2 } ;  { x ↔ a2  * y ↔ b2 }       { x ↔ b2  * y ↔ a2 }           *x  =  b2;}  ?? (Read) { x, y, a2 }; { x ↦ a2 * y ↦ b }  →  { x ↦ b * y ↔ a2 }  |  [let  b2  =  *y;] ?? (Read) {x,y}; {xHa*yHb} → {xHb*yHa}  | |let a2 = *x; ??
void swap(loc x, loc y) { let a2 = *x; let b2 = *y; *X = b2; *y = a2;
●  Towards Curry-Howard: the Lambda-Calculus 。 Intuitionistic Logic and the idea of Constructive Proofs 。 Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic  Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair
87

●  Towards Curry-Howard: the Lambda-Calculus ●  Intuitionistic Logic and the idea of Constructive Proofs ●  Types and Simply-Typed Lambda Calculus ●  Curry-Howard Correspondence: Propositions as Types, Proofs = Programs ●   Polymorphic Lambda-Calculus ●  Dependent Types and Quantifying over Values ●   Curry-Howard for Practitioners: Program Synthesis and Proof Repair

Small Scale Reflection for the Working Lean User
Vladimir Gladshtein ✉命D School of Computing, National University of Singapore, Singapore George PîrleaロッロSchool of Computing, National University of Singapore, Singapore Ilya Sergey日本0 School of Computing, National University of Singapore, Singapore
—— Abstract –
We present the design and implementation of the Small Scale Reflection proof methodology and tactic language ( a.k.a.  SSR) for the Lean 4 proof assistant.  Like its Coq predecessor SSReflect, our Lean 4 implementation, dubbed LeanSSR, provides powerful rewriting principles and means for effective management of hypotheses in the proof context. Unlike SSReflect for Coq, LeanSSR does not require explicit switching between the logical and symbolic representation of a goal, allowing for even more concise proof scripts that seamlessly combine deduction steps with proofs by computation. In this paper, we first provide a gentle introduction to the principles of structuring mechanised proofs using LeanSSR. Next, we show how the native support for metaprogramming in Lean 4 makes it possible to develop LeanSSR entirely within the proof assistant, greatly improving the overall experience of both tactic implementers and proof engineers. Finally, we demonstrate the utility of LeanSSR by conducting two case studies:  (a) porting a collection of Coq lemmas about sequences from the widely used Mathematical Components library and (b) reimplementing proofs in the finite set library of Lean’s mathlib4. Both case studies show significant reduction in proof sizes. Tuesday, 23 April, 14:30 To take away Formal proofs are functional programs in disguise; propositions are program types; writing a proof = constructing a program. Thinking in terms of Curry-Howard correspondence brings new insights allowing to combine and reuse ideas between Formal Mathematics and Computer Science slides of this talk (in case you missed it) Thanks! 90
● Xavier Leroy. The Curry-Howard correspondence today. xavierleroy.org/CdF/2018-2019/ ● Benjamin Pierce. Types and Programming Languages. MIT Press, 2002 ● Ilya Sergey. Programs and Proofs: Mechanizing Mathematics with Dependent Types ● Yves Bertot, Pierre Castéran. Interactive Theorem Proving and Program Development. ● David Thrane Christiansen. Functional Programming in Lean ● Ilya Sergey and Nadia Polikarpova. Structuring the Synthesis of Heap-Manipulating Programs ● Talia Ringer. Proof Repair. PhD Thesis, 2021 ● Kiran Gopinathan, Mayank Keoliya, Ilya Sergey. Mostly Automated Proof Repair for Verified Libraries, 2023