hazelgrove/hazelnut-dynamics-agda issues and pull requests

#56 - Add System F-style Polymorphism

Pull Request - State: open - Opened by Crazycolorz5 over 1 year ago

#55 - Rename FBoxed to FBoxedVal

Issue - State: closed - Opened by cyrus- about 6 years ago - 1 comment
Labels: final-artifact

#54 - update to the most recent version of Agda

Issue - State: closed - Opened by cyrus- about 6 years ago - 4 comments

#53 - add link to dockers-agda to README

Issue - State: closed - Opened by cyrus- about 6 years ago
Labels: final-artifact

#52 - prove preservation of binders-unique

Issue - State: open - Opened by ivoysey about 6 years ago

#51 - rename "expansion" to "elaboration"

Issue - State: closed - Opened by cyrus- about 6 years ago - 4 comments

#50 - prove the continuity theorem

Issue - State: closed - Opened by cyrus- about 6 years ago

#49 - clean house

Issue - State: closed - Opened by ivoysey about 6 years ago - 3 comments
Labels: meta

#48 - expand-ana-disjoint

Issue - State: closed - Opened by ivoysey about 6 years ago
Labels: metatheory of expansion

#47 - weaken-synth-expand

Issue - State: closed - Opened by ivoysey about 6 years ago - 1 comment
Labels: metatheory of expansion

#46 - mechanize the proofs in Sec. 4 (Instantiation and Commutativity)

Issue - State: open - Opened by cyrus- about 6 years ago
Labels: metatheory of instantiation

#45 - show that removing id casts doesn't change evaluation behaivour

Issue - State: open - Opened by ivoysey about 6 years ago
Labels: metatheory of expansion

#44 - id cast removal

Issue - State: closed - Opened by ivoysey over 6 years ago - 1 comment

#43 - alternative formulation of DCCast

Issue - State: closed - Opened by cyrus- over 6 years ago - 4 comments

#42 - rename correspondence theorem to generality

Issue - State: closed - Opened by cyrus- over 6 years ago

#41 - phrasing: dynamic -> internal expressions

Issue - State: closed - Opened by cyrus- over 6 years ago - 1 comment
Labels: meta

#40 - Resumption

Issue - State: closed - Opened by ivoysey over 6 years ago

#39 - Final confluence

Issue - State: closed - Opened by ivoysey over 6 years ago

#38 - Confluence

Issue - State: closed - Opened by ivoysey over 6 years ago - 8 comments

#37 - complete expansion

Issue - State: closed - Opened by ivoysey over 6 years ago
Labels: metatheory of expansion

#36 - modal stepping, determinism of stepping

Issue - State: open - Opened by ivoysey over 6 years ago - 4 comments
Labels: head scratchers

#35 - change the form of failed casts

Issue - State: closed - Opened by ivoysey over 6 years ago

#35 - change the form of failed casts

Issue - State: closed - Opened by ivoysey over 6 years ago

#34 - think about blame

Issue - State: open - Opened by cyrus- almost 7 years ago - 1 comment
Labels: head scratchers

#33 - remove casterr judgement and add term form + associated rules + refactor lemmas etc.

Issue - State: closed - Opened by ivoysey almost 7 years ago

#32 - quasi-readable canonical forms statements

Issue - State: closed - Opened by ivoysey almost 7 years ago

#32 - quasi-readable canonical forms statements

Issue - State: closed - Opened by ivoysey almost 7 years ago

#31 - remove red box premises

Issue - State: closed - Opened by ivoysey almost 7 years ago

#30 - canonical indeterminate forms for arrows

Issue - State: closed - Opened by ivoysey almost 7 years ago - 2 comments

#29 - revisit cast errors

Issue - State: closed - Opened by ivoysey almost 7 years ago - 3 comments

#28 - reformulate ITGround and ITExpand to use a "matched ground type" judgement

Issue - State: closed - Opened by cyrus- almost 7 years ago - 4 comments

#27 - rename CECastFinal to CECastFail

Issue - State: closed - Opened by ivoysey almost 7 years ago

#26 - double check quantification on all non-equality premises

Issue - State: closed - Opened by ivoysey almost 7 years ago - 3 comments

#25 - combine EALam and EALamHole

Issue - State: closed - Opened by cyrus- almost 7 years ago

#24 - cast-normal form

Issue - State: open - Opened by ivoysey almost 7 years ago - 1 comment
Labels: head scratchers

#23 - define hole instantiation and prove the instantiation theorem

Issue - State: closed - Opened by cyrus- almost 7 years ago - 1 comment
Labels: metatheory of instantiation

#22 - define the multi-step judgement

Issue - State: closed - Opened by cyrus- almost 7 years ago

#21 - break complete preservation down into complete expansion and complete preservation

Issue - State: closed - Opened by cyrus- almost 7 years ago - 6 comments

#20 - stepping shouldn't have a Delta in statement of complete progress

Issue - State: closed - Opened by cyrus- almost 7 years ago

#19 - state new canonical forms lemmas from notes

Issue - State: closed - Opened by cyrus- almost 7 years ago - 5 comments

#18 - this comment should say boxedval not val

Issue - State: closed - Opened by cyrus- almost 7 years ago

#17 - stepping shouldn't have a Delta in statement of preservation

Issue - State: closed - Opened by cyrus- almost 7 years ago - 1 comment

#16 - this line shouldn't mention "sums and products"

Issue - State: closed - Opened by cyrus- almost 7 years ago

#15 - README

Issue - State: closed - Opened by cyrus- almost 7 years ago - 2 comments
Labels: meta

#14 - prove progress checks

Issue - State: closed - Opened by ivoysey almost 7 years ago

#13 - remove marks on all holes

Issue - State: closed - Opened by ivoysey almost 7 years ago - 2 comments

#12 - prove substitution lemmas

Issue - State: closed - Opened by cyrus- almost 7 years ago - 1 comment
Labels: type safety

#11 - double check ITCast rule

Issue - State: closed - Opened by ivoysey almost 7 years ago - 1 comment

#10 - state and prove commutativity

Issue - State: closed - Opened by ivoysey almost 7 years ago - 1 comment
Labels: metatheory of instantiation

#9 - catalog hypothetical judgements, prove all the structural rules about them

Issue - State: closed - Opened by ivoysey almost 7 years ago - 1 comment
Labels: meta

#8 - prove typed expansion

Issue - State: closed - Opened by ivoysey almost 7 years ago - 2 comments
Labels: metatheory of expansion

#7 - prove complete preservation

Issue - State: closed - Opened by ivoysey almost 7 years ago - 2 comments

#6 - prove complete progress

Issue - State: closed - Opened by ivoysey almost 7 years ago

#5 - prove progress checks: errors don't step

Issue - State: closed - Opened by ivoysey almost 7 years ago - 4 comments

#4 - prove progress checks: indets don't step

Issue - State: closed - Opened by ivoysey almost 7 years ago

#3 - prove progress

Issue - State: closed - Opened by ivoysey almost 7 years ago

#2 - prove preservation

Issue - State: closed - Opened by ivoysey almost 7 years ago
Labels: type safety

#1 - change holes to have the tick vs check

Issue - State: closed - Opened by ivoysey over 7 years ago

GitHub / hazelgrove/hazelnut-dynamics-agda issues and pull requests