Ordered Adjoint Logic (Extended Version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914579258277888 |
|---|---|
| author | Roshal, Sophia Pfenning, Frank |
| author_facet | Roshal, Sophia Pfenning, Frank |
| contents | Ordered logics and type systems have been used in a variety of applications
including computational linguistics, memory allocation, stream processing,
logical frameworks, parametricity, and enforcing security protocols. In most
formulations, ordered types are also linear, requiring each resource to be
used exactly once. Prior work by Kanovich et al. has investigated calculi
that relax this constraint through subexponentials within a linear ordered
logic. We generalize their work by using adjoint modalities to combine logics
with varying fine-grained structural properties, including weakening, left
contraction, right contraction, left mobility, and right mobility. We show
that the resulting sequent calculus admits cut elimination.
We further provide a natural deduction formulation in which structural rules
are implicit, and show that proof checking for this system is decidable. This
makes it a suitable foundation for an expressive adjoint programming language
or logical framework. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_19112 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Ordered Adjoint Logic (Extended Version) Roshal, Sophia Pfenning, Frank Logic in Computer Science Programming Languages Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most formulations, ordered types are also linear, requiring each resource to be used exactly once. Prior work by Kanovich et al. has investigated calculi that relax this constraint through subexponentials within a linear ordered logic. We generalize their work by using adjoint modalities to combine logics with varying fine-grained structural properties, including weakening, left contraction, right contraction, left mobility, and right mobility. We show that the resulting sequent calculus admits cut elimination. We further provide a natural deduction formulation in which structural rules are implicit, and show that proof checking for this system is decidable. This makes it a suitable foundation for an expressive adjoint programming language or logical framework. |
| title | Ordered Adjoint Logic (Extended Version) |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2605.19112 |