WG211/M13Igarashi

An E-learning System for the Formal Semantics of Computer Programs and Its Implementation by Program Generation by Atsushi Igarashi

In the first half of this talk, I introduce an e-learning system for teaching the formal semantics of computer programs. One of the main characteristics of the system is that students are supposed to write down derivation trees directly, without understanding tactics languages or even lambda-terms.

In the second half, I describe the current implementation of the system. The core of the system, which is a family of OCaml programs to decide whether a derivation tree given by a student is correct with respect to inference rules, is generated from specifications of formal systems such as operational semantics or type systems. I discuss several issues in building such a system from the view point of program generation and perspectives for MetaOCaml-like multi-stage programming languages.