Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Isabelle (proof assistant)

Related lectures (31)

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.

Coq: Overview

Introduces Coq and focuses on proving the theorem and_comm step by step.

Coq Workshop: Inductive Data Types and Proofs

Covers the definition of an inductive data type in Coq and how to build proofs interactively using tactics.

Coq Workshop: Introduction to Interactive Theorem Proving

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

Verifying Programs with Stainless

Explores the verification of programs using Stainless, focusing on functional correctness, proof assistants, and automation of reasoning tasks.

Proofs and Computations: A Journey Through Mathematical Theory

Explores historical mathematical proofs, decision problems, deductive systems, probabilistic and quantum proofs, and interactive proof systems.

Coq: Introduction

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

Automated Reasoning in Practice

Explores practical automated reasoning systems like TPTP, TSTP, and CASC, emphasizing the importance of consistency and future developments.

Linear Algebra: Implications and Equivalences

Explores implications and equivalences in linear algebra through examples and formal proofs.

Automated Reasoning: Formal Verification with LISA

Explores formal verification using the LISA proof assistant and the OCBSL Equivalence Checker.

Markov Chains: Applications and Coupled Chains

Covers Markov chains, coupled chains, and their applications, emphasizing the importance of irreducibility.

What is a Formal Proof?

Covers the concept of formal proof systems, their structure, and soundness.

Formal Proofs: Checking Invariants and Bounded Model Checking

Explores formal proofs, satisfiability problems, and inductive invariants using SAT queries in sequential circuits.

Finite Systems Expressed with Formulas

Explores encoding finite systems with boolean functions, propositional logic, inductive invariants, and formal proof systems.

Trustworthy Systems Research

Discusses the need for proven trustworthiness in computer systems and the rigorous approach to achieving true trustworthiness in critical systems.

Finite Automata: Recap

Covers the fundamentals of finite automata and formal languages.

Propositional Logic: Translations and Equivalences

Covers translating natural language to propositional logic and proving tautologies.

Propositional Resolution

Explores completeness in propositional logic, resolution on clauses, conjunctive form, unit resolution, SAT solvers, and proof generation.

LISA proof assistant: Formalisation and Verification Log in to Mediaspace to watch this video

Covers the LISA proof assistant's codebase organization, kernel package, FOL formalization, and proof package.

Data Abstraction: Modules and Specifications in Coq Log in to Mediaspace to watch this video

Discusses data abstraction in programming, focusing on modules and specifications in Coq.