Commit 5da00edc authored by Jonas Kastberg's avatar Jonas Kastberg

Nits

parent 9456e121
(** This file contains the definition of what semantic term types and semantic (** This file contains the definition of what semantic term types and semantic
session types are. A semantic term type is a unary (Iris) predicate on values, session types are. A semantic term type is a unary (Iris) predicate on values
as is customary in a logical relation for type soundness. A semantic session [val → iProp], as is customary in a logical relation for type soundness.
type is essentially an Actris protocol. A semantic session type is an Actris protocol [iProto].
There is a single variant [lty Σ k], which contains either a term type or a There is a single kinded variant [lty Σ k], which contains either a term type or a
session type, depending on the kind [k]. The reason for having a single type session type, depending on the kind [k]. The reason for having a single type
containing both term types and session types is that it allows for uniform containing both term types and session types is that it allows for uniform
definitions of polymorphic binders for term types and session types, instead of definitions of polymorphic binders for term types and session types, instead of
......
(** This file defines the semantic interpretations of sesssion types as Actris (** This file defines the semantic interpretations of session types as Actris
protocols. It includes session types for sending and receiving with session protocols. It includes session types for sending and receiving with session
polymorphism, as well as n-ary choice. Recursive protocols are defined in polymorphism, as well as n-ary choice. Recursive protocols are defined in
[model.v]. *) the model.v file. *)
From iris.algebra Require Export gmap. From iris.algebra Require Export gmap.
From actris.logrel Require Export model kind_tele. From actris.logrel Require Export model kind_tele.
From actris.channel Require Export channel. From actris.channel Require Export channel.
......
...@@ -4,21 +4,19 @@ term type formers of the type system. The semantic interpretation of a type ...@@ -4,21 +4,19 @@ term type formers of the type system. The semantic interpretation of a type
when a value belongs to a certain type. when a value belongs to a certain type.
The following types are defined: The following types are defined:
- [unit], [bool], [int]: basic types for unit, boolean and integer values, - [unit], [bool], [int]: basic types for unit, boolean and integer values,
respectively. respectively.
- [any]: inhabited by all values. - [any]: inhabited by all values.
- [A ⊸ B]: the type of affine functions from [A] to [B]. Affine functions can - [A ⊸ B]: the type of affine functions from [A] to [B]. Affine functions can
only be invoked once, since they might have captured affine resources. only be invoked once, since they might have captured affine resources.
- [A → B]: the type of non-affine (copyable) functions from [A] to [B]. These - [A → B]: the type of non-affine (copyable) functions from [A] to [B]. These
can be invoked any number of times. This is simply syntactic sugar for [copy can be invoked any number of times. This is simply syntactic sugar for
(A ⊸ B)]. [copy (A ⊸ B)].
- [A * B], [A + B], [∀ X, A], [∃ X, A]: products, sums, universal types, - [A * B], [A + B], [∀ X, A], [∃ X, A]: products, sums, universal types,
existential types. existential types.
- [copy A]: inhabited by those values in the type [A] which are copyable. In the - [copy A]: inhabited by those values in the type [A] which are copyable. In the
case of functions, for instance, functions (closures) which capture affine case of functions, for instance, functions (closures) which capture affine
resources are not copyable, whereas functions that do not capture resources resources are not copyable, whereas functions that do not capture resources are.
are.
- [copy- A]: acts as a kind of "inverse" to [copy A]. More precisely, we have - [copy- A]: acts as a kind of "inverse" to [copy A]. More precisely, we have
that [copy- (copy A) <:> A]. This type is used to indicate the results of that [copy- (copy A) <:> A]. This type is used to indicate the results of
operations that might consume a resource, but do not always do so, depending operations that might consume a resource, but do not always do so, depending
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment