Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

formalism: Clean up section on typed Hazelnut #8

Merged
merged 24 commits into from
Oct 10, 2023
Merged
Changes from 1 commit
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
70bf9aa
formalism: Give brief description of typed action calculus
mirryi Jun 6, 2023
b0084b6
formalism: Fix rules for marked zexp cursor erasure
mirryi Oct 8, 2023
4d9dc02
formalism: Use separate metavariable for marked zexps from untyped zexps
mirryi Oct 9, 2023
69fb9c2
formalism: Add missing marked zexp movement rules
mirryi Oct 9, 2023
17922d0
formalism: Name marked zexps MZExp
mirryi Oct 9, 2023
b616af5
formalism: Reorder fixed marked zexp rules to match order in precedin…
mirryi Oct 9, 2023
08b97ab
formalism: Add missing synthetic con rules for marked zexp
mirryi Oct 9, 2023
670d20e
formalism: Add missing synthetic zipper rules for marked zexp
mirryi Oct 9, 2023
220a6c0
formalism: Fix typed con rules with mode change
mirryi Oct 9, 2023
e90b605
formalism: Add mising analytic con rules for typed model
mirryi Oct 9, 2023
31c4924
formalism: Fix some analytic zipper rules for marked zexp lambda
mirryi Oct 9, 2023
0b53159
formalism: Fix and add missing analytic zipper rules for zippered mar…
mirryi Oct 10, 2023
7496f6e
formalism: Move type meet occurrences to premise in typed hazelnut model
mirryi Oct 10, 2023
74dd71e
formalism: Fix and add remaining analytic zipper rules for typed haze…
mirryi Oct 10, 2023
108637c
formalism: Remove spurious free variable zmexp definition
mirryi Oct 10, 2023
0c8acbb
formalism: Define mark erasure on zmexp -> zexp
mirryi Oct 10, 2023
698915b
formalism: Indicate domain/codomain for metafunctions
mirryi Oct 10, 2023
9518f09
formalism: Add quiver package
mirryi Oct 10, 2023
b315dff
formalism: Define erasure commutativity theorem
mirryi Oct 10, 2023
712ed56
formalism: Fix marked analysis judgment in typed hazelnut metatheorem…
mirryi Oct 10, 2023
69c917e
formalism: Give correctness metatheorem for typed hazelnut in relatio…
mirryi Oct 10, 2023
51d99b7
formalism: Clean up formatting of metatheorem section for typed hazelnut
mirryi Oct 10, 2023
d2b9018
formalism: Add missing marked zexp well-formedness rules
mirryi Oct 8, 2023
cf7db28
formalism: Break well-formedness rules across two pages
mirryi Oct 10, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
formalism: Give brief description of typed action calculus
mirryi committed Oct 10, 2023

Verified

This commit was signed with the committer’s verified signature.
mirryi Eric Zhao
commit 70bf9aae28c33ac05132bd14a754b7134270eff6
4 changes: 4 additions & 0 deletions formalism/typed.tex
Original file line number Diff line number Diff line change
@@ -9,6 +9,10 @@

\section{Typed hazelnut}
\label{sec:typed}
We now give a description of a \emph{typed} version of the Hazelnut action calculus that
incorporates the marked lambda calculus to solve the problem of non-local hole fixes. Here, unlike
in the integration of the untyped version and the marked lambda calculus given in
\cref{sec:untyped}, remarking is performed only when necessary instead of after every action.

\nomechanization{}