Session 10

Big-step reduction, LJQ and 2 variants of LJQ-PCF

Big-step semantics

• https://www.cs.kent.ac.uk/people/staff/sao/documents/esop16.pdf Owens, Myreen, Kumar, Tan, "Functional Big-step Semantics"

Call-by value calculi

• https://www.sciencedirect.com/science/article/pii/0304397575900171 Plotkin, "Call-by-name, call-by-value and the lambda-calculus"
• https://person.dibris.unige.it/moggi-eugenio/ftp/lics89.pdf Moggi, "Computational lambda-calculus and monads"
• https://www.cs.cmu.edu/~rwh/pfpl/supplements/pcfv.pdf Harper, "PFPL Supplement: PCF By Value"

LJQ

• http://www.csl.sri.com/users/sgl/Work/Reports/cie.pdf Dyckhoff, Lengrand, "LJQ: A Strongly Focused Calculus for Intuitionistic Logic"
• https://hal.archives-ouvertes.fr/hal-00150284/document Dyckhoff, Lengrand, "Call-by-Value Lambda-calculus and LJQ"
• http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.304.6625&rep=rep1&type=pdf Lengrand, "Strong Normalisation of λLJQ"