%%% Typed Semantics for Standard ML (Internal Language)
%%%% Daniel Lee, Karl Crary, Robert Harper


sing/sources.cfg		% metatheory of singleton kinds


% general definitions
uninhabited.elf			% the uninhabited judgment (falsehood)
metrics.elf			% generic tree-style size metric


% definitions for constructors and kinds, depends on nothing
syntax-cnkd.elf			% syntax for constructors and kinds
static-semantics-cnkd.elf	% static semantics of constructors and kinds


% block stuff
blocks-predecls-cnkd.elf		
blocks-cnkd.elf			% blocks
worlds-adequacy-cnkd.elf



% locations, depends on nothing
syntax-loc.elf
judgments-loc.elf
loc-lemmas.elf



% system with explicit contexts, depends on cnkd
explicit-context.elf		% explicit contexts
lookup-context.elf
explicit-context-lemmas.elf
static-semantics-e.elf		% static semantics of constructors and kinds



% lemmas about the declarative constructor and kind system
uninhabited-lemmas-cnkd.elf	% things provable from falsehood
seq-lemmas-cnkd.elf		% lemmas about syntactic equality
reflexivity-kinds.elf
weakening-kinds-cnkd.elf		
antisymmetry-kinds.elf		% antisymmetry of kinds
strengthening-cnkd.elf



% conversions between implicit and explicit systems
explicit-metrics.elf
explicate-lemmas.elf		% cut theorems
explicate.elf			% explicate (implicit to explicit)
weakening-cnkd-e.elf
substitution-cnkd-e.elf
functionality-cnkd-e.elf
implicate-lemmas.elf		% various lemmas necessary for implicate
implicate.elf			% implicate (explicit to implicit)



% lemmas about the declarative constructor and kind system
% post explicit systen
functionality-cnkd.elf		%
validity-cnkd.elf		% SH 3.10
symmetry-kinds.elf		% SH 3.12.1
transitivity-kinds.elf		% transitivity of kinds. SH 3.12.2 and SH 3.13
functionality-full.elf		% full functionality. SH 3.14
inversions-cons.elf		% inversions on the typing of constructors



% higher-order singleton kinds and their properties
singleton-kinds.elf		% higher-order singleton kinds
singleton-lemmas.elf		% admissible singleton rules, straight from SH
constructor-beta.elf		% constructor beta rules, straight from SH



% definitions for signatures, depends on cnkd
syntax-sigs.elf			% syntax for signatures
static-semantics-sigs.elf	% static semantics of signatures
worlds-adequacy-sigs.elf



% lemmas about the declarative signature system
uninhabited-lemmas-sigs.elf	% things provable from falsehood
seq-lemmas-sigs.elf		% lemmas about syntactic equality
fst-sg-lemmas.elf		% lemmas about fst
weakening-kinds-sigs.elf		
reflexivity-sigs.elf		% reflexivity of signatures
validity-sigs.elf
symmetry-sigs.elf		% symmetry of signatures
antisymmetry-sigs.elf		% anti-symmetry of signatures
transitivity-sigs.elf		% transivity of signature subtyping



% explicit system for sigs, depends on cnkd and cnkd-explicit
static-semantics-sigs-e.elf
explicit-metrics-sigs.elf
explicate-lemmas-sigs.elf
explicate-sigs.elf
functionality-sigs-e.elf
implicate-lemmas-sigs.elf
implicate-sigs.elf
functionality-sigs.elf



% location typings, depends on locations and constructors
syntax-lt.elf
judgments-lt.elf
lt-lemmas.elf			% lemmas about locations



% projectibility, depends on nothing. two point lattice
projectibility.elf		% projectibility lattice
projectibility-lemmas.elf	% lemmas about the projectibility lattice



% definitions for terms and modules, depends on cnkd, sg, loc, lt
syntax-tmmd.elf			% syntax for terms and modules
static-semantics-tmmd.elf	% static semantics of terms and modules



% blocks and worlds for terms and modules
blocks-predecls-tmmd.elf
blocks-tmmd.elf
worlds-adequacy-tmmd.elf



% lemmas about the declarative term and module system
uninhabited-lemmas-tmmd.elf	% things provable from falsehood
seq-lemmas-tmmd.elf		% lemmas about syntactic equality
fst-md-lemmas.elf		% lemmas about fst
weakening-lt.elf		% weakening for locations
substitution-terms.elf		% substituting terms
validity-tmmd.elf
substitution-mods.elf
inversions-terms.elf		% inversions on the typing of terms (needs vdt)
subderivations.elf		% subderivation lemmas
inversions-mods.elf		% inversion lemmas for modules




% stores and store typings
% store depends on loc, tm. store-typings depend on cn, kd, tm, md, loc, lt, st
store.elf			% representation of a dynamic store
store-typing.elf		% judgment for well-formed stores
uninhabited-lemmas-ltst.elf	% things provable from falsehood
store-typing-lemmas.elf		% lemmas about store typings
preservation-lemmas.elf		% more lemmas about store typings 



% dynamic judgments, depends on cn, kd, tm, md, loc, lt, st
value.elf			% dynamic values
raises.elf			% raises judgment
dynamic-semantics.elf		% dynamic semantics
notstuck.elf			% definition of not stuck




% type safety 1
seq-lemmas-dyn.elf		% lemmas about syntactic equality
proj-val-lemma.elf		% proves module values are projectible
canonical-forms-mods.elf	% canonical forms lemmas for mods
progress-lemmas-mods.elf	% progress factoring lemmas for modules
preservation-raises.elf		% shows raises always carry a "tagged" value
preservation-fst.elf		% shows that operational semantics respects fst




% constructor equality inversions
correspondence.thm		% correspondence with the singleton kind calculus
inequalities.elf		% vacuous constructor equalities
inversions-deq.elf		% inversions for constructor equalities



% type safety 2
canonical-forms-terms.elf	% canonical forms lemmas for terms
progress-lemmas-terms.elf	% progress factoring lemmas for terms
progress.elf			% progress for terms and modules
preservation.elf		% preservation for terms and modules