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"