scholarly journals A General Adequacy Result for a Linear Functional Language

1994 ◽  
Vol 1 (22) ◽  
Author(s):  
Torben Braüner
Keyword(s):  
General Result ◽  
Functional Programming ◽  
Linear Functional ◽  
Linear Logic ◽  
Domain Theory ◽  
Main Concern ◽  
Functional Language ◽  
Stable Domain ◽  
Categorical Semantics ◽  
Intuitionistic Linear Logic

A main concern of the paper will be a Curry-Howard interpretation of Intuitionistic Linear Logic. It will be extended with recursion, and the resulting functional programming language will be given operational as well as categorical semantics. The two semantics will be related by soundness and adequacy results. The main features of the categorical semantics are that convergence/divergence behaviour is modelled by a strong monad, and that recursion is modelled by ``linear fixpoints'' induced by CPO structure on the hom-sets. The ``linear fixpoints'' correspond to ordinary fixpoints in the category of free coalgebras w.r.t. the comonad used to interpret the ``of course'' modality. Concrete categories from (stable) domain theory satisfying the axioms of the categorical model are given, and thus adequacy follows in these instances from the general result.

scholarly journals A Model of Intuitionistic Affine Logic from Stable Domain Theory (Revised and Expanded Version)

1994 ◽  
Vol 1 (27) ◽  
Author(s):  
Torben Braüner
Keyword(s):  
Alternative Model ◽  
Linear Logic ◽  
Canonical Model ◽  
Domain Theory ◽  
Left Adjoint ◽  
Stable Maps ◽  
Stable Domain ◽  
Intuitionistic Linear Logic ◽  
Coherence Spaces

Girard worked with the category of coherence spaces and continuous stable maps and observed that the functor that forgets the linearity of linear stable maps has a left adjoint. This fundamental observation gave rise to the discovery of Linear Logic. Since then, the category of coherence spaces and linear stable maps, with the comonad induced by the adjunction, has been considered a canonical model of Linear Logic. Now, the same phenomenon is present if we consider the category of pre dI domains and continuous stable maps, and the category of dI domains and linear stable maps; the functor that forgets the linearity has a left adjoint. This gives an alternative model of Intuitionistic Linear Logic. It turns out that this adjunction can be factored in two adjunctions yielding a model of Intuitionistic Affine Logic; the category of pre dI domains and affine stable functions. It is the goal of this paper to show that this category is actually a model of Intuitionistic Affine Logic, and to show that this category moreover has properties which make it possible to use it to model convergence/divergence behaviour and recursion.

scholarly journals Relating Categorical Semantics for Intuitionistic Linear Logic

2005 ◽  
Vol 13 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Maria Emilia Maietti ◽  
Paola Maneggia ◽  
Valeria de Paiva ◽  
Eike Ritter
Keyword(s):  
Linear Logic ◽  
Categorical Semantics ◽  
Intuitionistic Linear Logic

scholarly journals Propositions as sessions

2014 ◽  
Vol 24 (2-3) ◽  
pp. 384-418 ◽  
Author(s):  
PHILIP WADLER
Keyword(s):  
Linear Functional ◽  
Linear Logic ◽  
Functional Language ◽  
Session Types ◽  
Deadlock Freedom ◽  
First Time ◽  
Standard Presentation

AbstractContinuing a line of work by Abramsky (1994), Bellin and Scott (1994), and Caires and Pfenning (2010), among others, this paper presents CP, a calculus, in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), Hondaet al. (1998), and Gay & Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yields a language free from races and deadlock, where race and deadlock freedom follows from the correspondence to linear logic.

Lilac: a functional programming language based on linear logic

1994 ◽  
Vol 4 (4) ◽  
pp. 395-433 ◽  
Author(s):  
Ian Mackie
Keyword(s):  
Programming Language ◽  
Functional Programming ◽  
Linear Logic ◽  
Reconstruction Algorithm ◽  
Linear Term ◽  
Control Information ◽  
Functional Programming Language ◽  
Type Reconstruction ◽  
And Control ◽  
Intuitionistic Linear Logic

AbstractWe take Abramsky's term assignment for Intuitionistic Linear Logic (the linear term calculus) as the basis of a functional programming language. This is a language where the programmer must embed explicitly the resource and control information of an algorithm. We give a type reconstruction algorithm for our language in the style of Milner's W algorithm, together with a description of the implementation and examples of use.

Program equivalence in a linear functional language

2000 ◽  
Vol 10 (2) ◽  
pp. 167-190 ◽  
Author(s):  
G. M. BIERMAN
Keyword(s):  
Linear Functional ◽  
Linear Logic ◽  
Type Systems ◽  
Functional Languages ◽  
Functional Language ◽  
Program Equivalence ◽  
Principal Theorem ◽  
Contextual Equivalence

Researchers have recently proposed that for certain applications it is advantageous to use functional languages whose type systems are based upon linear logic: so-called linear functional languages. In this paper we develop reasoning techniques for programs in a linear functional language, linPCF, based on their operational behaviour. The principal theorem of this paper is to show that contextual equivalence of linPCF programs can be characterised coinductively. This characterisation provides a tractable method for reasoning about contextual equivalence, and is used in three ways:[bull ] A number of useful contextual equivalences between linPCF programs is given.[bull ] A notion of type isomorphism with respect to contextual equivalence, called operational isomorphism, is given. In particular the types !ϕ[otimes ]!ψ and !(ϕ&ψ) are proved to be operationally isomorphic.[bull ] A translation of non-strict PCF into linPCF is shown to be adequate, but not fully abstract, with respect to contextual equivalence.

Linear types and approximation

2000 ◽  
Vol 10 (6) ◽  
pp. 719-745 ◽  
Author(s):  
MICHAEL HUTH ◽  
ACHIM JUNG ◽  
KLAUS KEIMEL
Keyword(s):  
Full Subcategory ◽  
Linear Logic ◽  
Domain Theory ◽  
Classical Domain ◽  
Complete Distributivity ◽  
Linear Types ◽  
Continuous Lattices

We study continuous lattices with maps that preserve all suprema rather than only directed ones. We introduce the (full) subcategory of FS-lattices, which turns out to be *-autonomous, and in fact maximal with this property. FS-lattices are studied in the presence of distributivity and algebraicity. The theory is extremely rich with numerous connections to classical Domain Theory, complete distributivity, Topology and models of Linear Logic.

scholarly journals Generalized Bounded Linear Logic and its Categorical Semantics

2021 ◽  
pp. 226-246
Author(s):  
Yōji Fukihara ◽  
Shin-ya Katsumata
Keyword(s):  
Linear Logic ◽  
Cut Elimination ◽  
Grading System ◽  
Bounded Linear ◽  
The Core ◽  
Categorical Structure ◽  
Categorical Semantics

AbstractWe introduce a generalization of Girard et al.’s called (and its affine variant ). It is designed to capture the core mechanism of dependency in , while it is also able to separate complexity aspects of . The main feature of is to adopt a multi-object pseudo-semiring as a grading system of the !-modality. We analyze the complexity of cut-elimination in , and give a translation from with constraints to with positivity axiom. We then introduce indexed linear exponential comonads (ILEC for short) as a categorical structure for interpreting the $${!}$$ ! -modality of . We give an elementary example of ILEC using folding product, and a technique to modify ILECs with symmetric monoidal comonads. We then consider a semantics of using the folding product on the category of assemblies of a BCI-algebra, and relate the semantics with the realizability category studied by Hofmann, Scott and Dal Lago.

VoDKA: Developing a Video-on-Demand Server using Distributed Functional Programming

2005 ◽  
Vol 15 (3) ◽  
pp. 403-430 ◽  
Author(s):  
VICTOR M. GULIAS ◽  
MIGUEL BARREIRO ◽  
JOSE L. FREIRE
Keyword(s):  
Real World ◽  
Functional Programming ◽  
Building Blocks ◽  
Video On Demand ◽  
Functional Language ◽  
Control Software ◽  
On Demand ◽  
System Requirements ◽  
Cable Company ◽  
Process Composition

In this paper, we present some experience of using the concurrent functional language Erlang to implement a distributed video-on-demand server. For performance reasons, the server is deployed in a cheap cluster made from off-the-shelf components. The demanding system requirements, in addition to the complex and ever-changing domain, suggested a highly flexible and scalable architecture as well as a quite sophisticated control software. Functional programming played a key role in the development, allowing us to identify functional abstractions throughout the system. Using these building blocks, large configurations can be defined using functional and process composition, reducing the effort spent on adapting the system to the frequent changes in requirements. The server evolved from a prototype that was the result of a project supported by a regional cable company, and it is currently being used to provide services for real-world users. Despite our initial concerns, efficiency has not been a major issue.

Sign in / Sign up

Export Citation Format

Share Document