Séance de cours
Cette séance de cours couvre les langues d'Isar, ML et Scala. Il commence par un aperçu du cadre Isabelle/Pure et du cadre logique qu'il fournit. La séance de cours se déroule ensuite dans le langage de la preuve Isabelle/Isar, montrant comment les règles pures sont transformées en systèmes de preuve. Des exemples de règles et de preuves de déduction naturelle sont présentés, ainsi que des applications dans les définitions inductives et les preuves. La séance de cours traite également de l'approche LCF, des couches pour la programmation du système Isabelle et de l'architecture d'interface émergente à l'aide de Scala. Il se termine par un résumé linguistique de Isabelle/Isar, Isabelle/ML et Isabelle/Scala, mettant en évidence leurs caractéristiques et leur efficacité.