Reference. Relating Message Passing and Shared Memory, Proof-Theoretically
Cite
Cited by (4)
CoLF Logic Programming as Infinitary Proof Exploration chen-2025-colf
Substructural Parametricity aberle-2025-substructural
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.
Implementing a Message-Passing Interpretation of the Semi-Axiomatic Sequent Calculus (Sax) francalanza-2024-implementing
Adjoint Natural Deduction jang-2024-adjoint
Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.
Cites 26 works (4 here)
With notes (4)
Data Layout from a Type-Theoretic Perspective deyoung-2023-data
The specifics of data layout can be important for the efficiency of functional programs and interaction with external libraries. In this paper, we develop a type-theoretic approach to data layout that could be used as a typed intermediate language in a compiler or to give a programmer more control. Our starting point is a computational interpretation of the semi-axiomatic sequent calculus for intuitionistic logic that defines abstract notions of cells and addresses. We refine this semantics so addresses have more structure to reflect possible alternative layouts without fundamentally departing from intuitionistic logic. We then add recursive types and explore example programs and properties of the resulting language.
Session Types as Intuitionistic Linear Propositions caires-2010-session
A mixed linear and non-linear logic: Proofs, terms and models: Extended abstract bentonMixedLinearNonlinear1995
Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad. This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.
Linear logic girard_linear_1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
External (22)
- Back to futures (2022)
- A message-passing interpretation of adjoint logic (2020)
- Semi-axiomatic sequent calculus (2020)
- Linear logic propositions as session types (2014)
- Foundations of Software Science and Computational Structures (2012)
- Propositions as sessions (2012)
- Relating state-based and process-based concurrency through linear logic (full-version) (2009)
- A judgmental deconstruction of modal logic (2009)
- Syntax vs. semantics: A polarized approach (2005)
- The π-Calculus: A Theory of Mobile Processes (2001)
- Efficient resource management for linear logic proof search (2000)
- Pipelining with Futures (1999)
- Communicating and Mobile Systems: the π-Calculus (1999)
- Linearity and the pi-calculus (1996)
- CONCUR’93 (1993)
- Logic Programming with Focusing Proofs in Linear Logic (1992)
- ECOOP’91 European Conference on Object-Oriented Programming (1991)
- Linear logic and lazy computation (1987)
- MULTILISP: a language for concurrent symbolic computation (1985)
- Listlessness is better than laziness: Lazy evaluation and garbage collection at compile-time (1984)
- The formulae-as-types notion of construction (1969)
- Functionality in Combinatory Logic (1934)