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

Lecture

The Languages of Isabelle: Isar, ML, and Scala

Description

This lecture covers the languages of Isabelle, focusing on Isar, ML, and Scala. It starts with an overview of the Isabelle/Pure framework and the logical framework it provides. The lecture then delves into the Isabelle/Isar proof language, showcasing how Pure rules are transformed into proof schemes. Examples of Natural Deduction rules and proofs are presented, along with applications in inductive definitions and proofs. The lecture also discusses the LCF approach, the layers for Isabelle system programming, and the emerging interface architecture using Scala. It concludes with a language summary of Isabelle/Isar, Isabelle/ML, and Isabelle/Scala, highlighting their characteristics and efficiency.

Official source

Ontological neighbourhood

Theoretical computer science

Programming language theory: High-level programming languages

Logic

Classical logic: First-order logic

Related concepts (32)

Proof assistant

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer. A recent effort within this field is making these tools use artificial intelligence to automate the formalization of ordinary mathematics.

Isabelle (proof assistant)

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring yet supporting explicit proof objects. Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods.

Proof theory

Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

Standard ML

Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers. Standard ML is a modern dialect of ML, the language used in the Logic for Computable Functions (LCF) theorem-proving project. It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML.

Constructive proof

In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existence proof or pure existence theorem), which proves the existence of a particular kind of object without providing an example. For avoiding confusion with the stronger concept that follows, such a constructive proof is sometimes called an effective proof.

Related lectures (34)

Coq Workshop: Introduction to Interactive Theorem Proving

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

Concept of Proof in Mathematics

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

Proofs: Logic, Mathematics & Algorithms

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

Coq: Overview

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

Coq Workshop: Inductive Data Types and Proofs