Semantic Analysis of Normalisation for Directional Logic Programming

workshop
bidirectional typechecking
categorical semantics
classical linear logic
directional logic programming
Authors
Affiliations

Vikraman Choudhury

Università di Bologna, Bologna, Italy

Neel Krishnaswami

University of Cambridge, UK

Ariadne Si Suo

University of Cambridge, UK

Published

January 1, 2025

Abstract

This work is about using directional logic programming to give foundations to mode-correct bidirectional type systems [2, 6.2]. Reddy[5] uses a term language for classical linear logic, adapted from Abramsky’s Linear Chemical Abstract Machine (LCHAM) [1], to give a typed calculus for directional logic programs. We give a categorical semantics to Reddy’s calculus, using polycategories. We give normalisation results for this calculus, which shows how to evaluate logic queries to normal forms, that gives output substitutions indicating whether queries fail or succeed.

Keywords

bidirectional typechecking, categorical semantics, classical linear logic, directional logic programming

Back to top

Citation

BibTeX citation:
@inproceedings{choudhury2025,
  author = {Choudhury, Vikraman and Krishnaswami, Neel and Si Suo,
    Ariadne},
  title = {Semantic {Analysis} of {Normalisation} for {Directional}
    {Logic} {Programming}},
  booktitle = {Fourth Workshop on the Implementation of Type Systems},
  date = {2025},
  url = {https://vikraman.org/papers/choudhury-krishnaswami-suo-2025/},
  langid = {en},
  abstract = {This work is about using directional logic programming to
    give foundations to mode-correct bidirectional type systems {[}2,
    \textbackslash S 6.2{]}. Reddy{[}5{]} uses a term language for
    classical linear logic, adapted from Abramsky’s Linear Chemical
    Abstract Machine (LCHAM) {[}1{]}, to give a typed calculus for
    directional logic programs. We give a categorical semantics to
    Reddy’s calculus, using polycategories. We give normalisation
    results for this calculus, which shows how to evaluate logic queries
    to normal forms, that gives output substitutions indicating whether
    queries fail or succeed.}
}
For attribution, please cite this work as:
Choudhury, Vikraman, Neel Krishnaswami, and Ariadne Si Suo. 2025. “Semantic Analysis of Normalisation for Directional Logic Programming.” Fourth Workshop on the Implementation of Type Systems, accepted. https://vikraman.org/papers/choudhury-krishnaswami-suo-2025/.