# Computational Adequacy for Substructural Lambda Calculi

@inproceedings{Zamdzhiev2020ComputationalAF, title={Computational Adequacy for Substructural Lambda Calculi}, author={Vladimir Zamdzhiev}, booktitle={ACT}, year={2020} }

Substructural type systems, such as affine (and linear) type systems, are type systems which impose restrictions on copying (and discarding) of variables, and they have found many applications in computer science, including quantum programming. We describe one linear and one affine type systems and we formulate abstract categorical models for both of them which are sound and computationally adequate. We also show, under basic assumptions, that interpreting lambda abstractions via a monoidal… Expand

#### References

SHOWING 1-10 OF 20 REFERENCES

LNL-FPC: The Linear/Non-linear Fixpoint Calculus

- Computer Science, Mathematics
- Log. Methods Comput. Sci.
- 2021

A type system with mixed linear and non-linear recursive types called LNL-FPC (the linear/non-linear fixpoint calculus) and a new technique for solving recursive domain equations within cartesian categories by constructing the solutions over pre-embeddings is described. Expand

Mixed linear and non-linear recursive types

- Computer Science, Mathematics
- Proc. ACM Program. Lang.
- 2019

A type system with mixed linear and non-linear recursive types called LNL-FPC (the linear/non-linear fixpoint calculus) and a new technique for solving recursive domain equations within the category CPO by constructing the solutions over pre-embeddings is described. Expand

Semantics for a Lambda Calculus for String Diagrams

- 2020

Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment… Expand

A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract)

- Mathematics, Computer Science
- FoSSaCS
- 2008

A categorical semantics for a call-by-value linear lambda calculus, which was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation, and gives a combination of a monad and a comonad that makes the present paper interesting. Expand

Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams

- Computer Science, Mathematics
- LICS
- 2018

This work presents an adequacy result for the diagram-free fragment of the language which corresponds to a modified version of Benton and Wadler's adjoint calculus with recursion, and extends the language with general recursion and proves soundness. Expand

Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory

- Computer Science, Mathematics
- FoSSaCS
- 2020

This paper constructs a sound categorical model for the quantum programming language QPL and provides the first detailed semantic treatment of user-defined inductive datatypes in quantum programming, and shows the denotational interpretation is invariant with respect to big-step reduction. Expand

A categorical model for a quantum circuit description language

- Computer Science, Mathematics
- QPL
- 2017

This paper formalizes a small, but useful fragment of Quipper called Proto-Quipper-M, which is type-safe and has a formal denotational and operational semantics, and defines the programming language to fit the model. Expand

Linear logic, monads and the lambda calculus

- Mathematics, Computer Science
- Proceedings 11th Annual IEEE Symposium on Logic in Computer Science
- 1996

Models of intuitionistic linear logic also provide models of Moggi's computational metalanguage and the adjoint presentation of these models and the associated adjoint calculus is used to show that three translations of the lambda calculus into the computational metalanguages correspond exactly to three translations, due mainly to Girard, of intuitionist logic into intuitionisticlinear logic. Expand

A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract)

- Mathematics, Computer Science
- CSL
- 1994

Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Expand

Towards a quantum programming language

- Computer Science
- Mathematical Structures in Computer Science
- 2004

This paper describes the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types, and has an interesting denotational semantics in terms of complete partial orders of superoperators. Expand