Towards Unifying (Co)induction and Structural Control
Résumé
In this work-in-progress paper, we extend hybrid multiplicative-additive linear logic with modalities for recursion so that infinite formulas and proofs correspond to (co)inductive types and programs. Working towards a unified logical framework, we consider various approaches to incorporating limited rules of weakening and contraction that reuse the hybrid structure.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)