Lectures related to Hoare Logic: Foundations and Applications

Introduction to Coq: Arithmetic Expressions and Evaluators

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

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.

Lambda Calculus and Type Safety: An Overview

Provides an overview of lambda calculus, type safety, and type inference in programming languages.

Coq Workshop: Introduction to Interactive Theorem Proving

Introduces Coq, an interactive theorem assistant based on the Curry-Howard isomorphism.

An Introduction to Iris: Higher-Order Concurrent Separation Logic

Introduces Iris, a logical framework for reasoning about safety and correctness of concurrent higher-order imperative programs, emphasizing its unique characteristics and applications.

Inductive Propositions: Reasoning and Evaluation Techniques

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

Simply Typed Lambda Calculus: Foundations and Properties

Covers the simply typed lambda calculus, focusing on its syntax, semantics, and type system properties such as progress and preservation.

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.

Termination Analysis using Dependency Pairs

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

Proofs: Logic, Mathematics & Algorithms

Explores proof concepts, techniques, and applications in logic, mathematics, and algorithms.

Semantics in Computer Language Processing: Understanding Meaning

Covers the semantics of programming languages, focusing on the Add language and the role of rewriting rules and CK machines in understanding meaning.

Stainless Verification System Tutorial

Introduces Stainless, an open-source tool for verifying Scala programs, covering language, modeling, verification tips, and inner workings.

Propositions as Types: Logic and Programming Correspondence

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

Concept of Proof in Mathematics

Delves into the concept of proof in mathematics, emphasizing the importance of evidence and logical reasoning.

The Languages of Isabelle: Isar, ML, and Scala

Explores the languages of Isabelle, focusing on Isar, ML, and Scala, covering proof schemes, Natural Deduction rules, inductive definitions, and the LCF approach.

Hoare Logic: Strongest Postcondition and Weakest Precondition

Covers Hoare logic, strongest postcondition, and weakest precondition for simplifying proofs in imperative programming.

Effective Altruism: AI Safety and Governance

Covers effective altruism in AI safety, focusing on programming semantics and memory management.

Sparsest Cut: ARV Theorem

Covers the proof of the Bourgain's ARV Theorem, focusing on the finite set of points in a semi-metric space and the application of the ARV algorithm to find the sparsest cut in a graph.

Untitled