On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep

WG211/M13Igarashi: Difference between revisions

From WG 2.11
Jump to navigationJump to search
VisualWikitext
Created page with "''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 introduc..."
 
No edit summary
 
Line 1: Line 1:
''An E-learning System for the Formal Semantics of Computer Programs and Its Implementation by Program Generation'' by Atsushi Igarashi
''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
In the first half of this talk, I introduce an e-learning
system for teaching the formal semantics of computer programs.  One
system for teaching the formal semantics of computer programs.  One
of the main characteristics of the system is that students are
of the main characteristics of the system is that students are
supposed to write down derivation trees directly, without
supposed to write down derivation trees directly, without
understanding tactics languages or even lambda-terms.
understanding tactics languages or even lambda-terms.


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

Latest revision as of 17:38, 10 March 2014

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.

Retrieved from "http://mw.hh.se/wg211/index.php?title=WG211/M13Igarashi&oldid=993"