hazelgrove/hazelnut-dynamics-agda

Issues

• update to the most recent version of Agda

  #54 opened 6 years ago by cyrus-
  4

• prove preservation of binders-unique

  #52 opened 6 years ago by ivoysey
  0

• add link to dockers-agda to README

  #53 opened 6 years ago by cyrus-
  0

• Rename FBoxed to FBoxedVal

  #55 opened 6 years ago by cyrus-
  1

• rename "expansion" to "elaboration"

  #51 opened 6 years ago by cyrus-
  4

• clean house

  #49 opened 6 years ago by ivoysey
  3

• prove the continuity theorem

  #50 opened 6 years ago by cyrus-
  0

• prove substitution lemmas

  #12 opened 6 years ago by cyrus-
  1

• phrasing: dynamic -> internal expressions

  #41 opened 6 years ago by cyrus-
  1

• show that removing id casts doesn't change evaluation behaivour

  #45 opened 6 years ago by ivoysey
  0

• mechanize the proofs in Sec. 4 (Instantiation and Commutativity)

  #46 opened 6 years ago by cyrus-
  0

• define hole instantiation and prove the instantiation theorem

  #23 opened 6 years ago by cyrus-
  1

• catalog hypothetical judgements, prove all the structural rules about them

  #9 opened 6 years ago by ivoysey
  1

• state and prove commutativity

  #10 opened 6 years ago by ivoysey
  1

• weaken-synth-expand

  #47 opened 6 years ago by ivoysey
  1

• expand-ana-disjoint

  #48 opened 6 years ago by ivoysey
  0

• README

  #15 opened 6 years ago by cyrus-
  2

• cast-normal form

  #24 opened 7 years ago by ivoysey
  1

• id cast removal

  #44 opened 6 years ago by ivoysey
  1

• prove typed expansion

  #8 opened 7 years ago by ivoysey
  2

• complete expansion

  #37 opened 7 years ago by ivoysey
  0

• alternative formulation of DCCast

  #43 opened 7 years ago by cyrus-
  4

• rename correspondence theorem to generality

  #42 opened 7 years ago by cyrus-
  0

• modal stepping, determinism of stepping

  #36 opened 7 years ago by ivoysey
  4

• think about blame

  #34 opened 7 years ago by cyrus-
  1

• Confluence

  #38 opened 7 years ago by ivoysey
  8

• break complete preservation down into complete expansion and complete preservation

  #21 opened 7 years ago by cyrus-
  6

• Final confluence

  #39 opened 7 years ago by ivoysey
  0

• Resumption

  #40 opened 7 years ago by ivoysey
  0

• prove complete progress

  #6 opened 7 years ago by ivoysey
  0

• quasi-readable canonical forms statements

  #32 opened 7 years ago by ivoysey
  0

• change the form of failed casts

  #35 opened 7 years ago by ivoysey
  0

• remove casterr judgement and add term form + associated rules + refactor lemmas etc.

  #33 opened 7 years ago by ivoysey
  0

• revisit cast errors

  #29 opened 7 years ago by ivoysey
  3

• canonical indeterminate forms for arrows

  #30 opened 7 years ago by ivoysey
  2

• remove red box premises

  #31 opened 7 years ago by ivoysey
  0

• prove progress checks

  #14 opened 7 years ago by ivoysey
  0

• reformulate ITGround and ITExpand to use a "matched ground type" judgement

  #28 opened 7 years ago by cyrus-
  4

• state new canonical forms lemmas from notes

  #19 opened 7 years ago by cyrus-
  5

• rename CECastFinal to CECastFail

  #27 opened 7 years ago by ivoysey
  0

• double check quantification on all non-equality premises

  #26 opened 7 years ago by ivoysey
  3

• combine EALam and EALamHole

  #25 opened 7 years ago by cyrus-
  0

• define the multi-step judgement

  #22 opened 7 years ago by cyrus-
  0

• this comment should say boxedval not val

  #18 opened 7 years ago by cyrus-
  0

• stepping shouldn't have a Delta in statement of complete progress

  #20 opened 7 years ago by cyrus-
  0

• this line shouldn't mention "sums and products"

  #16 opened 7 years ago by cyrus-
  0

• stepping shouldn't have a Delta in statement of preservation

  #17 opened 7 years ago by cyrus-
  1

• double check ITCast rule

  #11 opened 7 years ago by ivoysey
  1

• remove marks on all holes

  #13 opened 7 years ago by ivoysey
  2

• prove complete preservation

  #7 opened 7 years ago by ivoysey
  2