Semantic Analysis of Normalisation for Directional Logic Programming
summary
Claims a formal bridge: bidirectional type checking becomes directional logic programs whose evaluation is normalisation as cut reductions in classical linear logic. Gives a categorical semantics of Reddy’s calculus using polycategories, proves normalization theorems that turn queries into output substitutions (success or failure) and extends the language with inductive and coinductive contexts so mode correctness is decidable by typechecking the directional program and nontermination from naive subtyping is avoided.
AI-written summary · about
chapters (6)
- 0:00Type checking as proof reductions
- 3:19Bidirectional typing and mode correctness
- 10:32Fine-grained mode systems
- 17:21Type checkers as logic programs
- 20:12Mode correctness foundation
- 22:41Q&A
related talks
24mFrom Enhanced Coinduction towards Enhanced Induction
28mReasoning about Distributed Reconfigurable Systems
25mStep-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch...
20mInductive diagrams for causal reasoning
15mProducts of Recursive Programs for Hypersafety Verification
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
25mRelax! The Semilenient Core of Choreographic Programming (Functional Pearl)
20mDeciding Asynchronous Hyperproperties for Recursive Programs