Isabelle quick start guide

For many, the process of transforming a textbook mathematical proof into a formal document remains mysterious. Here, we look at a straightforward example. Dirichlet’s approximation theorem states that each real number has a rational approximation with a relatively small denominator. The proof combines an application of the pigeonhole principle...

One of the key tensions in theorem proving is between reasoning about things and using them in serious computations. One way to address this tension is through computational reflection: treating logical formulas as executable code, when you can. The first realisation of this idea was the Boyer/Moore theorem prover, which was initially created to...

Just in time for the holiday break, here are some small exercises to build your skills. The subject matter is the prime numbers: specifically, the maximum exponent of a prime divisor of a number. A skeleton Isabelle theory file is available, containing all statements of the theorems and necessary definitions or boilerplate, but no proofs. Your...

A well-known technique to speed up computer code is to re-order some steps, for example to lift a costly operation out of a loop. In logic, when we can choose what inference to do next, making the right choices yields an exponentially shorter proof. Also in the λ-calculus we sometimes have a choice of reduction steps: the possible outcomes...

The λ-calculus has had a pervasive impact on computer science – and not just in functional programming languages, most of which can be viewed as extended λ-calculi, but even in modern systems programming languages such as Rust. Polymorphic type checking emerged in the context of the typed λ-calculus and now exists (to some extent) in many modern...