Ups at 16:38, 10 March 2014

2014-03-10T16:38:00Z

Ups: 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..."

2014-03-10T16:37:41Z

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

New page

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

← Older revision		Revision as of 18:38, 10 March 2014
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.

WG211/M13Igarashi - Revision history

Ups at 16:38, 10 March 2014

Ups: 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..."