Mini-ML language and natural semantics

Computation and Deduction
Chapters 1-5
Author: Frank Pfenning

mini-ml.elf     --- expressions
eval.elf	--- evaluation judgment
value.elf       --- value judgments
val-sound.elf   --- value soundness proof
closed.elf      --- closed and open judgments
tp.elf          --- types
tpinf.elf       --- typing judgment
tp-preserve.elf --- type preservation proof

examples.quy    --- example queries

sources.cfg     --- standard configuration

Additional material

sources1.cfg    --- pure LF configuration
eval1.elf       --- evaluation judgment in pure LF

eval2.elf       --- evaluation judgment in declarative order