Session 9

Three bidirectional tricks: semiannotated lambdas, detalized errors and LJT checker derivation

• Chlipala, Petersen, Harper, "Strict Bidirectional Type Checking" (в частности, раздел 3.3 A half-annotated form)
• Refutation in Logic
• Negri, "Proofs and countermodels in non-classical logics"
• O’Hearn, "Incorrectness Logic"
• Puech, "Proofs, upside down: A functional correspondence between natural deduction and the sequent calculus"