Cette séance de cours présente Amyli, un minuscule langage fonctionnel prenant en charge les fonctions récursives, avec une syntaxe abstraite pour les termes et la sémantique opérationnelle. Il couvre l'exécution des programmes, les règles de type et la solidité à travers le progrès et la préservation, y compris les preuves et les exemples.