| Dear all, I proudly present the online material of an Isabelle/HOL course that was giving as part of the “Parisian Master of Research in Computer Science”(MPRI)- Programme, jointly run by University de Paris, the ENS Ulm and my institution, the University of Paris-Saclay. [The course has its roots in a series of lectures I was giving over the years, starting at the ETH in 2005]. It has both a theoretic track presented as an animated slide-set with accompanying podcast and a series of practical lab courses (“TP”’s). The theoretical part attempts to establish links to theoretical foundations taught in parallel classes (lambda-calculus, semantic) at the MPRI, as far as this vis possible in a 5-units course … A part from the title, all material is in English ... All comments welcome! Burkhart |