sequent-calc
sequent-calc copied to clipboard
Published
20 hours ago •
clayrat
clayrat
Experiments with sequent calculi
Sequent Calc
Experiments with sequent calculi and abstract machines
References
| Folder/file | Reference |
|---|---|
MuMuTilde |
https://www.irif.fr/~emiquey/these/ |
SeqCalc |
https://github.com/freebroccolo/sequent-calculus |
Levy |
http://plzoo.andrej.com/language/levy.html |
KAM.Alg |
Swierstra, "From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine" https://bitbucket.org/sergei.romanenko/agda-krivine-machine/ |
Duploid |
https://github.com/freebroccolo/agda-syntactic-duploids/ |
KSF |
Kunze, Smolka, Forster, "Formal Small-step Verification of a Call-by-value Lambda Calculus Machine" |
ABS |
Ariola, Bohannon, Sabry, "Sequent calculi and abstract machines" |
ClasByNeed |
Ariola, Downen, Herbelin, Nakata, Saurin, "Classical call-by-need sequent calculi: The unity of semantic artifacts" |
NDSC |
https://wenkokke.github.io/2016/one-lambda-calculus-many-times/ |
L.Spiwack |
http://assert-false.net/arnaud/papers/A%20dissection%20of%20L.pdf |
L.Scherer |
http://gallium.inria.fr/~scherer/research/L/tutorial-talk.pdf |
LJ |
Brock-Nannestad, Guenot, Gustafsson, "Computation in Focused Intuitionistic Logic" |
Lambda.Untyped.Strong.HOR |
Kluge, "Abstract Computing Machines" (sec 6.4) |
Lambda.Untyped.Strong.KN |
Cregut, "Strongly Reducing Variants of the Krivine Abstract Machine" |
ABDM |
Ager, Biernacki, Danvy, Midtgaard, "From Interpreter to Compiler and Virtual Machine: A Functional Derivation" |
Forcing.CoquandHaber |
Coquand, Jaber, "A computational interpretation of forcing in Type Theory" |
LJ.LJMSE |
Santo, Matthes, Pinto, "Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi" |
Kappa |
https://en.wikipedia.org/wiki/Kappa_calculus Megacz, "Abstraction Elimination for Kappa Calculus" |
Lambda.T |
Alves, Fernandez, Florido, Mackie, "Godel’s System T Revisited" |
LambdaMu.Delim.Top |
Ariola, Herbelin, Sabry, "A type-theoretic foundation of delimited continuations" Herbelin, Ghilezan, "An approach to call-by-name delimited continuations" |
Lambda.PCFV |
Harper, "PFPL Supplement: PCF By Value" |
clayrat