Lectures related to Lean (proof assistant)

Inductive Propositions: Understanding Evaluation in Coq

Covers inductive propositions in Coq, focusing on evaluation rules for arithmetic expressions and their applications in defining partial and non-deterministic functions.

Big-step semantics: Defining arithmetic expressions and commands

Covers the definition of a simple programming language and its big-step semantics, including arithmetic expressions and imperative commands.

Logic Programming Techniques: Automated Proof Search and Unification

Covers logic programming concepts, focusing on automated proof search and unification techniques in Coq.

Introduction to Proof Scripting: Basics of Ltac

Introduces the basics of proof scripting in Coq, focusing on the Ltac language and its tactics for managing proofs effectively.

Propositions as Types: Logic and Programming Correspondence

Explores the relationship between logic proofs and programming evidence through the Curry-Howard Correspondence.

Untitled