WG211/M13Igarashi

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

n 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.