Simply Typed Lambda-Calculus with a small-step, allocation semantics.
This is an attempt to get a feel for #Twelf with a problem somewhere
between the trivial simply typed lambda-calculus with a large-step
semantics (a Twelf documentation example) and Karl Crary's TALT
formalization (which is too complex to be useful for a novice).
Problems from the basic metatheory of System F<::
1a Transitivity of Subtyping
1b Transitivity of Subtyping with Records
2a Type Safety for Pure F<:
2b Type Safety for with Records and Pattern Matching
3 Testing and Animating with Respect to the Semantics
Problems from the basic metatheory of System F<::
1a Transitivity (559 lines)
1b with Records (1227 lines)
2a Type Safety (745 lines)
2b with Records and Pattern Matching (4176 lines)
Type checking: higher-order abstract syntax, judgments-as-types.
• Unification-based argument synthesis, definition mechanism.
• Logic programming interpretation: backchaining (cf λ-Prolog)
• Coverage and totality checking: a prover for ∀∃ formulae.
tatics via Judgments-as-Types:
• Typing: of : tm → tp → Type.
• Example: arr-I : (x : tm → of x T1 → of (F x) T2) → of (lam F ) (arr T1 T2).
Dynamics via Plotkin’s SOS:
• Transition: step : tm → tm → Type.
• Example: beta : step (ap (lam F ) M) (F M)
https://www.cs.cornell.edu/people/fluet/twelf/alloc-sem/README.txt
https://www.cs.cornell.edu/people/fluet/twelf/
https://www.cs.cmu.edu/~rwh/talks/FP22.pdf
gpg -vv -r myid -e -a name, /
npub1wh…hjvu8
2024-02-18 08:13:29
Author Public Key
npub1wharawc5r9yp4g3ar5ha4rs0ve0xyl85z43rqmlhudxv6txs0sjsqhjvu8Published at
2024-02-18 08:13:29Event JSON
{
"id": "86f216dca3f8e969076d23bbade2cf2d87c4e7d6effcd32b9d78e3dd918efe3c",
"pubkey": "75fa3ebb1419481aa23d1d2fda8e0f665e627cf41562306ff7e34ccd2cd07c25",
"created_at": 1708244009,
"kind": 1,
"tags": [
[
"t",
"twelf"
],
[
"content-warning",
"todo note to self"
],
[
"proxy",
"https://emacs.ch/users/brokenix/statuses/111951479418058176",
"activitypub"
]
],
"content": "Simply Typed Lambda-Calculus with a small-step, allocation semantics. \n\nThis is an attempt to get a feel for #Twelf with a problem somewhere\nbetween the trivial simply typed lambda-calculus with a large-step\nsemantics (a Twelf documentation example) and Karl Crary's TALT\nformalization (which is too complex to be useful for a novice).\nProblems from the basic metatheory of System F\u003c::\n1a Transitivity of Subtyping\n1b Transitivity of Subtyping with Records\n2a Type Safety for Pure F\u003c:\n2b Type Safety for with Records and Pattern Matching\n3 Testing and Animating with Respect to the Semantics\nProblems from the basic metatheory of System F\u003c::\n1a Transitivity (559 lines)\n1b with Records (1227 lines)\n2a Type Safety (745 lines)\n2b with Records and Pattern Matching (4176 lines)\nType checking: higher-order abstract syntax, judgments-as-types.\n• Unification-based argument synthesis, definition mechanism.\n• Logic programming interpretation: backchaining (cf λ-Prolog)\n• Coverage and totality checking: a prover for ∀∃ formulae.\ntatics via Judgments-as-Types:\n• Typing: of : tm → tp → Type.\n• Example: arr-I : (x : tm → of x T1 → of (F x) T2) → of (lam F ) (arr T1 T2).\nDynamics via Plotkin’s SOS:\n• Transition: step : tm → tm → Type.\n• Example: beta : step (ap (lam F ) M) (F M)\nhttps://www.cs.cornell.edu/people/fluet/twelf/alloc-sem/README.txt\nhttps://www.cs.cornell.edu/people/fluet/twelf/\nhttps://www.cs.cmu.edu/~rwh/talks/FP22.pdf",
"sig": "f519e334fd8f139c181ecfa2fa2e7568ad1251462d9f1b531a5c414bb663ebc222ad2bd677858120ec2dbc638d8ef0392f8887beaa4135def22e88d8e28c0708"
}