Introduction to Proof Scripting: Basics of Ltac

About
Privacy
Disclaimer

Graph Chatbot

Related lectures (30)

Page 1 of 3

Introduction to Coq: Arithmetic Expressions and Evaluators

Covers the basics of Coq, focusing on arithmetic expressions, evaluation, and proof techniques.

Hoare Logic: Foundations and Applications

Covers Hoare Logic, its foundations, applications, and significance in program verification.

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.

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.

Inductive Propositions: Reasoning and Evaluation Techniques

Discusses inductive propositions, their definitions, and applications in reasoning and evaluation techniques in Coq.

Coq: Introduction

Introduces Coq, covering defining propositions, proving theorems, and using tactics.

Propositions as Types: Logic and Programming Correspondence

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

Formal Logic: Proofs and Sets

Covers the basics of formal logic, focusing on logical expressions and mathematical proofs.

Termination Analysis using Dependency Pairs

Explores automated termination analysis using dependency pairs, covering classical and modern techniques, annual competitions, and tools like AProVE.