## Abstract

Linear logic provides an elegant framework for modelling stateful, imperative and concurrent systems by viewing a context of assumptions as a set of resources. However, mechanizing the meta-theory of such systems remains a challenge, as we need to manage and reason about mixed contexts of linear and intuitionistic assumptions.

We present Lincx, a contextual linear logical framework with first-class mixed contexts. Lincx allows us to model (linear) abstract syntax trees as syntactic structures that may depend on intuitionistic and linear assumptions. It can also serve as a foundation for reasoning about such structures. Lincx extends the linear logical framework LLF with first-class (linear) contexts and an equational theory of context joins that can otherwise be very tedious and intricate to develop. This work may be also viewed as a generalization of contextual LF that supports both intuitionistic and linear variables, functions, and assumptions.

We describe a decidable type-theoretic foundation for Lincx that only characterizes canonical forms and show that our equational theory of context joins is associative and commutative. Finally, we outline how Lincx may serve as a practical foundation for mechanizing the meta-theory of stateful systems.

We present Lincx, a contextual linear logical framework with first-class mixed contexts. Lincx allows us to model (linear) abstract syntax trees as syntactic structures that may depend on intuitionistic and linear assumptions. It can also serve as a foundation for reasoning about such structures. Lincx extends the linear logical framework LLF with first-class (linear) contexts and an equational theory of context joins that can otherwise be very tedious and intricate to develop. This work may be also viewed as a generalization of contextual LF that supports both intuitionistic and linear variables, functions, and assumptions.

We describe a decidable type-theoretic foundation for Lincx that only characterizes canonical forms and show that our equational theory of context joins is associative and commutative. Finally, we outline how Lincx may serve as a practical foundation for mechanizing the meta-theory of stateful systems.

Originalsprog | Engelsk |
---|---|

Titel | 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings |

Forlag | Springer |

Publikationsdato | 2017 |

Sider | 530-555 |

ISBN (Trykt) | 978-3-662-54433-4 |

ISBN (Elektronisk) | 978-3-662-54434-1 |

DOI | |

Status | Udgivet - 2017 |

Navn | Lecture Notes in Computer Science |
---|---|

Vol/bind | 10201 |

ISSN | 0302-9743 |