search
attachments
weblink
advanced
Overview
Content Tools
PRL Seminar for Friday December 2
Finally tagless, partially evaluated:
Tagless staged interpreters for simpler typed languages
Chung-chieh Shan (joint work with Jacques Carette and Oleg Kiselyov)
This "functional necklace" aims to change how you try to write your next interpreter: by deforesting the object language, to exhibit more static safety in a simpler type system. We show how easy it is to build a family of interpreters for a typed object language (such as the simply typed lambda calculus) in a typed metalanguage (such as Haskell or ML) that preserve types without using dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The interpreters include an evaluator, a compiler, a partial evaluator, and call-by-name and call-by-value CPS transformers.
Our main idea is to encode abstract syntax using cogen functions rather than data constructors. In other words, we represent object terms not in an initial algebra but in an arbitrary algebra. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformation. Our encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck.
This Friday’s seminar will take place in Upson 5126 from 12:05-1:00PM.
PRL Seminar for Nov 18, 2011
A Conversation with Moshe Vardi
Join in a discussion with Professor Moshe Vardi on the topic of Logic in Computer Science.
This Friday’s seminar will take place in Upson 5126 from Noon-1P.
The PRL Seminar has been postponed for this week. We are planning a Seminar for next Friday (11/18) with more details to follow.
Presented at the November 4, 2011 PRL Seminar
Join us as we expand our discussion of the Simple Consensus Algorithm. This example illustrates many features of Event Logic and of the practical use of Mark's notion of programmable event classes and how Event ML and Nuprl cooperate to produce correct-by-construction code.
We will also illustrate how we can introduce diversity into the code at a high level and multiply it as we compile the protocol to production languages.
This Friday’s seminar will take place in Upson 5126 from Noon-1P