Lecture

The Languages of Isabelle: Isar, ML, and Scala

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

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.

Proof by contradiction

In logic, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Although it is quite freely used in mathematical proofs, not every school of mathematical thought accepts this kind of nonconstructive proof as universally valid. More broadly, proof by contradiction is any form of argument that establishes a statement by arriving at a contradiction, even when the initial assumption is not the negation of the statement to be proved.

Mathematical proof

A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation".

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.

Related lectures (64)

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.

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.

Introduction to Coq: Arithmetic Expressions and Evaluators