An Introduction to Lambda Calculus and Functional Programming Languages (Short course 1)

Dr. RODRIGO MACHADO

An Introduction to Interactive Theorem Proving with Isabelle/HOL (Short course 2)

Dr. ALFIO RICARDO DE BRITO MARTINI

Both in computer science and in mathematical logic, a proof assistant or an interactive theorem prover is a software that helps in the construction of formal proofs through an man-machine collaboration. In this course, we will present the Isabelle/HOL system for specification and verification. Isabelle is a generic system for the implementation of logical formalisms. Isabelle/HOL is the specialization of Isabelle for Higher Order Logic, where the term HOL can be understood through the following equation: HOL = Functional Programming + Logic. Isabelle/HOL is equipped with powerful tools for specification, e.g., data types, inductive definitions and functions with complex pattern matching. Proofs are conducted with the structured language Isar (Intelligible semi-automated reasoning). Isar allows the construction of structured proofs which are  readable by people and machine as well. In particular, we will introduce the necessary constructions for the specification and reasoning of (possibly recursive) function definitions as well as discrete structures like sets, relations and graphs. As a case study, we will use these tools to formalize semantics of a small imperative language. We will consider the traditional denotational, operational and axiomatics (Hoare) approaches to formal semantics of programming languages.