Polarized type theory in Twelf, for delimited control and
monadic reflection.

Companion to: "Polarity and the logic of delimited continuations"

Version: May 2010
Noam Zeilberger

context.elf	contexts and substitutions
positive.elf	positive fragment of generic type system
negative.elf	negative fragment of generic type system
generic.elf	some generic (derivable) value/continuation combinators
dummy.elf	dummy dictionary entries (Twelf hack)
dynamic.elf	generic operational semantics
poldict.elf	definition of polarized connectives and recursive types
runtime.lf	"native" arithmetic library
runtime-ffi.lf	"FFI" to native arithmetic
prelude.elf	some syntactic sugar/library routines
control.elf	derived effect-typing system for delimited control
filinski.elf	monadic reflection

Note: to run these files in Twelf CVS, auto-freezing must be turned off
(in emacs, "C-c < autoFreeze false").
