< Retour au sommaire

Skeletal Semantics by Example

Alan Schmitt le

Lieu: Amphithéâtres 33/34

Abstract

Skeletal Semantics is both a meta-language to describe semantics of programming languages (skel) and several tools to manipulate these semantics. We present skel through several examples, highlighting how complex features can be captured in a readable way using monads. We then briefly introduce some tools that take these formalizations as input, to generate OCaml interpreters and Coq formalizations.

Reference

M Bodin, P Gardner, T Jensen, A Schmitt Skeletal semantics and their interpretations Proceedings of the ACM conference on Programming Languages (POPL), 2019