|
|
|
|
-Q theories/lib semantics.lib
|
|
|
|
|
-Q theories/type_systems semantics.ts
|
|
|
|
|
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
|
|
|
|
|
-arg -w -arg -notation-overridden
|
|
|
|
|
# Cannot use non-canonical projections as it causes massive unification failures
|
|
|
|
|
# (https://github.com/coq/coq/issues/6294).
|
|
|
|
|
-arg -w -arg -redundant-canonical-projection
|
|
|
|
|
# we use Restart for demoing purposes, sometimes
|
|
|
|
|
-arg -w -arg -undo-batch-mode
|
|
|
|
|
|
|
|
|
|
# library stuff
|
|
|
|
|
theories/lib/maps.v
|
|
|
|
|
theories/lib/sets.v
|
|
|
|
|
theories/lib/debruijn.v
|
|
|
|
|
theories/lib/facts.v
|
|
|
|
|
|
|
|
|
|
# STLC
|
|
|
|
|
theories/type_systems/stlc/lang.v
|
|
|
|
|
theories/type_systems/stlc/notation.v
|
|
|
|
|
theories/type_systems/stlc/untyped.v
|
|
|
|
|
theories/type_systems/stlc/types.v
|
|
|
|
|
theories/type_systems/stlc/logrel.v
|
|
|
|
|
theories/type_systems/stlc/parallel_subst.v
|
|
|
|
|
|
|
|
|
|
# Extended STLC
|
|
|
|
|
theories/type_systems/stlc_extended/lang.v
|
|
|
|
|
theories/type_systems/stlc_extended/notation.v
|
|
|
|
|
theories/type_systems/stlc_extended/types.v
|
|
|
|
|
theories/type_systems/stlc_extended/types_sol.v
|
|
|
|
|
theories/type_systems/stlc_extended/bigstep.v
|
|
|
|
|
theories/type_systems/stlc_extended/bigstep_sol.v
|
|
|
|
|
theories/type_systems/stlc_extended/ctxstep.v
|
|
|
|
|
theories/type_systems/stlc_extended/ctxstep_sol.v
|
|
|
|
|
theories/type_systems/stlc_extended/parallel_subst.v
|
|
|
|
|
theories/type_systems/stlc_extended/logrel.v
|
|
|
|
|
theories/type_systems/stlc_extended/logrel_sol.v
|
|
|
|
|
|
|
|
|
|
# System F
|
|
|
|
|
theories/type_systems/systemf/lang.v
|
|
|
|
|
theories/type_systems/systemf/notation.v
|
|
|
|
|
theories/type_systems/systemf/types.v
|
|
|
|
|
theories/type_systems/systemf/types_sol.v
|
|
|
|
|
theories/type_systems/systemf/tactics.v
|
|
|
|
|
theories/type_systems/systemf/bigstep.v
|
|
|
|
|
theories/type_systems/systemf/church_encodings.v
|
|
|
|
|
theories/type_systems/systemf/parallel_subst.v
|
|
|
|
|
theories/type_systems/systemf/logrel.v
|
|
|
|
|
theories/type_systems/systemf/logrel_sol.v
|
|
|
|
|
theories/type_systems/systemf/free_theorems.v
|
|
|
|
|
theories/type_systems/systemf/binary_logrel.v
|
|
|
|
|
theories/type_systems/systemf/binary_logrel_sol.v
|
|
|
|
|
theories/type_systems/systemf/existential_invariants.v
|
|
|
|
|
theories/type_systems/systemf/church_encodings_faithful.v
|
|
|
|
|
|
|
|
|
|
# SystemF-Mu
|
|
|
|
|
theories/type_systems/systemf_mu/lang.v
|
|
|
|
|
theories/type_systems/systemf_mu/notation.v
|
|
|
|
|
theories/type_systems/systemf_mu/types.v
|
|
|
|
|
theories/type_systems/systemf_mu/tactics.v
|
|
|
|
|
theories/type_systems/systemf_mu/pure.v
|
|
|
|
|
theories/type_systems/systemf_mu/pure_sol.v
|
|
|
|
|
theories/type_systems/systemf_mu/untyped_encoding.v
|
|
|
|
|
theories/type_systems/systemf_mu/parallel_subst.v
|
|
|
|
|
theories/type_systems/systemf_mu/logrel.v
|
|
|
|
|
theories/type_systems/systemf_mu/logrel_sol.v
|
|
|
|
|
|
|
|
|
|
# SystemF + Mu + State
|
|
|
|
|
theories/type_systems/systemf_mu_state/locations.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/lang.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/notation.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/types.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/types_sol.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/tactics.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/execution.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/parallel_subst.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/logrel.v
|
|
|
|
|
theories/type_systems/systemf_mu_state/logrel_sol.v
|
|
|
|
|
|
|
|
|
|
# By removing the # below, you can add the exercise sheets to make
|
|
|
|
|
#theories/type_systems/warmup/warmup.v
|
|
|
|
|
#theories/type_systems/warmup/warmup_sol.v
|
|
|
|
|
#theories/type_systems/stlc/exercises01.v
|
|
|
|
|
#theories/type_systems/stlc/exercises01_sol.v
|
|
|
|
|
#theories/type_systems/stlc/exercises02.v
|
|
|
|
|
#theories/type_systems/stlc/exercises02_sol.v
|
|
|
|
|
#theories/type_systems/stlc/cbn_logrel.v
|
|
|
|
|
#theories/type_systems/stlc/cbn_logrel_sol.v
|
|
|
|
|
#theories/type_systems/systemf/exercises03.v
|
|
|
|
|
#theories/type_systems/systemf/exercises03_sol.v
|
|
|
|
|
#theories/type_systems/systemf/exercises04.v
|
|
|
|
|
#theories/type_systems/systemf/exercises04_sol.v
|
|
|
|
|
#theories/type_systems/systemf/exercises05.v
|
|
|
|
|
#theories/type_systems/systemf/exercises05_sol.v
|
|
|
|
|
#theories/type_systems/systemf_mu/exercises06.v
|
|
|
|
|
#theories/type_systems/systemf_mu/exercises06_sol.v
|
|
|
|
|
#theories/type_systems/systemf_mu_state/exercises07.v
|
|
|
|
|
#theories/type_systems/systemf_mu_state/exercises07_sol.v
|
