Skip to main content

Module functions

oxilean_std::session_types

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

acquire_ty
Acquire : SharedMemType β†’ SType β†’ SType Acquire a lock, then continue with a typed session.
affine_type_ty
AffineType : Type β†’ Prop Predicate for affine types (used at most once).
ambience_compatibility_ty
AmbienceCompatibility : Choreography β†’ GType β†’ Prop The choreography is compatible with the ambient global type.
app
app2
app3
arrow
async_dual_ty
AsyncDual : AsyncSType β†’ AsyncSType Dual of an asynchronous session type.
async_end_ty
AsyncEnd : AsyncSType Termination of an asynchronous session.
async_recv_ty
AsyncRecv : Type β†’ AsyncSType β†’ AsyncSType Asynchronous receive: eventually retrieve from buffer; continuation after receipt.
async_send_ty
AsyncSend : Type β†’ AsyncSType β†’ AsyncSType Asynchronous send: message is placed in a buffer; continuation does not wait.
async_stype_ty
AsyncSType : Type Asynchronous session type with buffered channels.
bang_ty
Bang : LLProp β†’ LLProp Exponential modality: !A β€” unrestricted use.
bool_ty
buffer_bound_ty
BufferBound : AsyncSType β†’ Nat β†’ Prop The buffer size is bounded by n; prevents unbounded queuing.
build_session_types_env
Build the session types environment.
bvar
cast_insertion_ty
CastInsertion : GSType β†’ SType β†’ GSType β†’ Prop Cast insertion: convert between gradual and static session types.
catch_ty
Catch : ExSType β†’ ExSType β†’ ExSType try S catch H β€” run S, if exception H is raised, switch to handler.
channel_ty
Channel : SType β†’ Type A typed channel: Chan S is a channel whose protocol is S.
choreography_consistency_ty
ChoreographyConsistency : Choreography β†’ Prop A choreography is consistent if all endpoint projections are compatible.
choreography_ty
Choreography : Type A global choreography: the global view of a multiparty protocol.
close_ty
close : Chan End β†’ Unit Close a finished channel.
coinductive_ty
Coinductive : SType β†’ Prop Coinductive (possibly infinite) session type.
cst
ctx_split_ty
CtxSplit : LinearCtx β†’ LinearCtx β†’ LinearCtx β†’ Prop Context splitting: the left context is the disjoint union of the right two.
curry_howard_ll_ty
CurryHowardLL : LLProp β†’ SType β†’ Prop The Curry-Howard correspondence between MILL propositions and session types.
cut_elim_ty
CutElim : Prop Cut elimination theorem for MILL: every proof can be made cut-free.
data_race_free_ty
DataRaceFree : SharedMemType β†’ Prop A shared memory protocol is data-race free by type structure.
deadlock_free_ty
DeadlockFree : Process β†’ Prop A process is deadlock-free if all reachable states are not stuck.
deadlock_freedom_thm_ty
DeadlockFreedomThm : βˆ€ (P : Process) (S : SType), WellTyped P S β†’ DeadlockFree P Deadlock freedom from type well-typedness.
dep_channel_ty
DepChannel : DepSType β†’ Type
dep_dual_ty
DepDual : DepSType β†’ DepSType
dep_end_ty
DepEnd : DepSType
dep_recv_ty
DepRecv : {T : Type} β†’ (T β†’ DepSType) β†’ DepSType ?x : T. S(x) β€” receive x of type T, continuation depends on x.
dep_send_msg_ty
DepSendMsg : {T : Type} β†’ {S : T β†’ DepSType} β†’ DepChan (DepSend S) β†’ (x : T) β†’ DepChan (S x)
dep_send_ty
DepSend : {T : Type} β†’ (T β†’ DepSType) β†’ DepSType !x : T. S(x) β€” send x of type T, continuation depends on x.
dep_stype_ty
DepSType : Type Dependent session types: the continuation type can depend on communicated values.
dual_end_ty
dual_end : dual End = End
dual_involutive_ty
dual_involutive : βˆ€ (S : SType), dual (dual S) = S
dual_send_ty
dual_send : βˆ€ (T : Type) (S : SType), dual (Send T S) = Recv T (dual S)
dual_ty
dual : SType β†’ SType Duality: swaps Send and Recv, swaps SChoice and SBranch.
dyn_stype_ty
DynSType : GSType The dynamic session type ? β€” completely unchecked at compile time.
dynamic_monitor_ty
DynamicMonitor : GSType β†’ Prop A session type that must be monitored at runtime.
end_ty
End : SType Session termination β€” the session has ended.
endpoint_projection_ty
EndpointProjection : Choreography β†’ Role β†’ LType Project a choreography onto a role’s local type.
equi_recursive_ty
EquiRecursive : SType β†’ Prop Predicate for equi-recursive session types (implicit fold/unfold).
eventual_delivery_ty
EventualDelivery : AsyncSType β†’ Prop Every message sent is eventually delivered (liveness guarantee).
ex_stype_ty
ExSType : Type Session types extended with exceptions and failure handling.
exception_safe_ty
ExceptionSafe : ExSType β†’ Prop A session type is exception-safe if all exceptions are handled.
expected_cost_ty
ExpectedCost : ProbSType β†’ Nat β†’ Prop Expected number of communication steps is bounded by n.
fault_tolerant_ty
FaultTolerant : ExSType β†’ Prop A process is fault-tolerant if it can recover from any exception.
fold_ty
Fold : SType β†’ SType Fold back a session type into a recursive form.
g_stype_ty
GSType : Type Gradual session types: mixing static and dynamic checking.
gchoice_ty
GChoice : Role β†’ Role β†’ GType β†’ GType β†’ GType p + q { G₁, Gβ‚‚ } β€” role p makes a choice communicated to q.
gcomm_ty
GComm : Role β†’ Role β†’ Type β†’ GType β†’ GType p β†’ q : T. G β€” role p sends a value of type T to role q, then continues as G.
gend_ty
GEnd : GType The end of the global protocol.
global_view_ty
GlobalView : GType β†’ Choreography Extract the global view (choreography) from a global type.
gradual_consistency_ty
GradualConsistency : GSType β†’ GSType β†’ Prop Gradual consistency: two session types agree on their static parts.
gradual_recv_ty
GradualRecv : Type β†’ GSType β†’ GSType Gradual receive: partially statically checked.
gradual_send_ty
GradualSend : Type β†’ GSType β†’ GSType Gradual send: partially statically checked.
grec_ty
GRec : (GType β†’ GType) β†’ GType Recursive global type: ΞΌX.G(X).
gtype_ty
GType : Type A global session type (the overall protocol from a bird’s-eye view).
ho_dual_ty
HODual : HOSType β†’ HOSType Dual of a higher-order session type.
ho_stype_ty
HOSType : Type Higher-order session types: channels can carry session channels.
impl_pi
infer_stype_ty
InferSType : Process β†’ SType β†’ Prop Session type inference judgment.
inference_complete_ty
InferenceComplete : Prop Completeness of session type inference.
inference_sound_ty
InferenceSound : Prop Soundness of session type inference.
is_value_ty
IsValue : Process β†’ Prop
iso_recursive_ty
IsoRecursive : SType β†’ Prop Predicate for iso-recursive session types (explicit fold/unfold).
lbranch_ty
LBranch : Role β†’ LType β†’ LType β†’ LType External choice from role r.
lchoice_ty
LChoice : Role β†’ LType β†’ LType β†’ LType Internal choice offered to role r.
lend_ty
LEnd : LType Session end from one participant’s perspective.
linear_ctx_ty
LinearCtx : Type A linear typing context: a finite map from names to (linear) types.
linear_safety_ty
LinearSafety : Process β†’ Prop A process is safe if channels are used linearly (exactly once).
linear_type_ty
LinearType : Type β†’ Prop Predicate asserting a type is linear (used exactly once).
linear_well_typed_ty
LinearWellTyped : LinearCtx β†’ Process β†’ SType β†’ Prop Typing judgment for linear processes.
list_ty
ll_prop_ty
LLProp : Type Propositions in multiplicative intuitionistic linear logic (MILL).
locally_consistent_ty
LocallyConsistent : LType β†’ Prop
lolli_ty
Lolli : LLProp β†’ LLProp β†’ LLProp Linear implication: A ⊸ B.
lrecv_ty
LRecv : Role β†’ Type β†’ LType β†’ LType ?p(T).L β€” receive T from role p, continue as L.
lsend_ty
LSend : Role β†’ Type β†’ LType β†’ LType !q(T).L β€” send T to role q, continue as L.
ltype_ty
LType : Type A local session type: the protocol from one participant’s perspective.
markov_chain_protocol_ty
MarkovChainProtocol : ProbSType β†’ Prop The probabilistic session type has a finite-state Markov chain interpretation.
mergeability_ty
Mergeability : LType β†’ LType β†’ Prop Two local types can be merged (for projection of choices not involving a role).
mutex_ty
Mutex : Type β†’ SharedMemType A mutex protecting a resource of type T.
nat_ty
par_ty
Par : LLProp β†’ LLProp β†’ LLProp Multiplicative disjunction: A β…‹ B.
participants_ty
Participants : GType β†’ List Role Extract the set of roles participating in a global type.
pi
principal_stype_ty
PrincipalSType : Process β†’ SType β†’ Prop The principal (most general) session type of a process.
prob_choice_ty
ProbChoice : SType β†’ SType β†’ Expr S₁ βŠ•[p] Sβ‚‚ β€” choose S₁ with probability p, Sβ‚‚ with probability 1-p.
prob_stype_ty
ProbSType : Type Probabilistic session type with Markov-chain semantics.
prob_termination_ty
Termination : ProbSType β†’ Prop The probabilistic session terminates with probability 1 (almost-sure termination).
process_ty
Process : Type The type of processes in the session calculus.
progress_thm_ty
ProgressThm : βˆ€ (P : Process) (S : SType), WellTyped P S β†’ IsValue P ∨ βˆƒ P', Reduces P P'
progress_ty
Progress : Process β†’ SType β†’ Prop Progress: a well-typed process either terminates or can take a step.
project_ty
project : GType β†’ Role β†’ LType Project a global type onto a specific role’s local type.
projection_sound_ty
ProjectionSound : βˆ€ (G : GType) (p : Role), WellFormed G β†’ LocallyConsistent (project G p) Soundness of projection: projections of well-formed globals are locally consistent.
prop
realization_ty
Realization : Choreography β†’ GType β†’ Prop A choreography is realized by a global type.
recv_chan_ty
RecvChan : SType β†’ HOSType β†’ HOSType ?Chan(S).T β€” receive a channel of type S, then continue as T.
recv_contravariant_ty
RecvContravariant : βˆ€ T S₁ Sβ‚‚, SSubtype S₁ Sβ‚‚ β†’ SSubtype (Recv T Sβ‚‚) (Recv T S₁) Receive is contravariant in the continuation (dual direction).
recv_msg_ty
recv_msg : {T : Type} β†’ {S : SType} β†’ Chan (Recv T S) β†’ (T Γ— Chan S) Receive a message from a channel.
recv_ty
Recv : Type β†’ SType β†’ SType ?T.S β€” receive a value of type T, then continue as S.
reduces_ty
Reduces : Process β†’ Process β†’ Prop One-step reduction relation.
release_ty
Release : SharedMemType β†’ SType β†’ SType Release a lock, then continue.
role_ty
Role : Type A participant role in a multiparty session.
sbranch_ty
SBranch : SType β†’ SType β†’ SType External choice: S₁ & Sβ‚‚ β€” offer both branches, peer selects.
schoice_ty
SChoice : SType β†’ SType β†’ SType Internal choice: S₁ βŠ• Sβ‚‚ β€” select one branch to send.
send_chan_ty
SendChan : SType β†’ HOSType β†’ HOSType !Chan(S).T β€” send a channel of type S, then continue as T.
send_covariant_ty
SendCovariant : βˆ€ T S₁ Sβ‚‚, SSubtype S₁ Sβ‚‚ β†’ SSubtype (Send T S₁) (Send T Sβ‚‚) Send is covariant in the continuation.
send_msg_ty
send_msg : {T : Type} β†’ {S : SType} β†’ Chan (Send T S) β†’ T β†’ Chan S Send a message along a channel.
send_ty
Send : Type β†’ SType β†’ SType !T.S β€” send a value of type T, then continue as S.
session_passing_ty
SessionPassing : HOSType β†’ Prop A higher-order session type that involves session-passing.
shared_mem_type_ty
SharedMemType : Type Session types for shared memory concurrency.
srec_ty
SRec : (SType β†’ SType) β†’ SType Iso-recursive session type: ΞΌX.S(X).
ssubtype_refl_ty
SSubtypeRefl : βˆ€ S, SSubtype S S
ssubtype_trans_ty
SSubtypeTrans : βˆ€ S₁ Sβ‚‚ S₃, SSubtype S₁ Sβ‚‚ β†’ SSubtype Sβ‚‚ S₃ β†’ SSubtype S₁ S₃
ssubtype_ty
SSubtype : SType β†’ SType β†’ Prop Behavioral subtyping: S₁ <: Sβ‚‚ means S₁ can be used where Sβ‚‚ is expected.
string_ty
stuck_ty
Stuck : Process β†’ Prop A process is stuck if it cannot reduce and is not a value.
stype_equiv_ty
STypeEquiv : SType β†’ SType β†’ Prop Bisimilarity / coinductive equality of session types.
stype_subst_ty
STypeSubst : Type A session type substitution.
stype_ty
SType : Type The type of binary session types.
stype_unify_ty
STypeUnify : SType β†’ SType β†’ STypeSubst β†’ Prop Unification of session types under a substitution.
subject_reduction_ty
SubjectReduction : Prop Subject reduction: typing is preserved by reduction.
svar_ty
SVar : Nat β†’ SType Session type variable (de Bruijn index).
tensor_ty
Tensor : LLProp β†’ LLProp β†’ LLProp Multiplicative conjunction: A βŠ— B.
throw_ty
Throw : Type β†’ ExSType Raise an exception of the given type, terminating the session.
type0
type_safety_ty
TypeSafety : Prop Type safety: well-typed processes do not go wrong.
unfold_preserves_dual_ty
UnfoldPreservesDual : βˆ€ S, dual (Unfold S) = Unfold (dual S)
unfold_ty
Unfold : SType β†’ SType Unfold one step of a recursive session type: ΞΌX.S(X) ↦ S(ΞΌX.S(X)).
unrestricted_type_ty
UnrestrictedType : Type β†’ Prop Predicate for unrestricted (reusable) types.
well_formed_ty
WellFormed : GType β†’ Prop A global type is well-formed if all roles are consistent and the protocol terminates.
well_typed_process_ty
WellTypedProcess : Process β†’ SType β†’ Prop
why_not_ty
WhyNot : LLProp β†’ LLProp Exponential modality: ?A β€” potential use.