(* Title: POPLmark/POPLmark.thy Author: Stefan Berghofer, TU Muenchen, 2005 *) theory POPLmark imports Basis begin section ‹Formalization of the basic calculus› text ‹ \label{sec:basic-calculus} In this section, we describe the formalization of the basic calculus without records. As a main result, we prove {\it type safety}, presented as two separate theorems, namely {\it preservation} and {\it progress}. › subsection ‹Types and Terms› text ‹ The types of System \fsub{} are represented by the following datatype: ›