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"