Pith. sign in

REVIEW 3 major objections 4 minor 20 references

Intrinsically-Typed Mechanized Semantics for Session Types

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper claims the first fully mechanized proof of type soundness and session fidelity for a realistic functional session-typed calculus, with both properties enforced by the semantics' own typing.

desk verdict A serious and useful Agda artifact whose headline claim outruns the proved results. read the letter →

arxiv 1908.02940 v1 pith:27T4U5RN submitted 2019-08-08 cs.PL

Peter Thiemann This is my paper · ORCID
classification cs.PL
keywords sessiontypesmechanizedproofAgdaintrinsicallytypedsemanticsCEKmachinelinearfidelitytypesoundness
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims to deliver the first fully mechanized proof of type soundness and session fidelity for a realistic functional session-typed calculus. It does so by implementing the semantics in Agda as an intrinsically typed, interruptible CEK machine, so that well-typedness of every machine state is forced by the type system rather than proved as a separate theorem. The machine maintains linearity through a resource splitting tree that tracks which thread holds which end of which channel. Type preservation and a relative progress property then hold by construction, because ill-typed states and duplicate channel uses cannot be expressed. Mechanized soundness proofs for session types are rare, and this work shows a path to machine-checked guarantees for a calculus with linearity, recursion, recursive sessions, and subtyping.

What carries the argument

The central object is the resource splitting tree: a binary tree of session-context splittings that distributes channel endpoints across values, environments, continuations, threads, and the thread pool, in parallel with the splitting of the linear typing context. This tree carries the argument because it makes linearity and unique ownership of channel ends structurally enforced: a resource can go entirely left, entirely right, or, when both ends are available, be split into positive and negative ends. The scheduler's step function and its matching functions traverse this tree to perform rendezvous, and the Junction type captures the two nested splittings needed to transfer resources between a sender and a receiver. The CEK machine is stuttering: expression-level decomposition issues Commands and yields to the scheduler for all serious effects such as communication, thread creation, and channel creation.

What would settle it

Take any closed program P and any one-step reduction P to Q in the intended small-step calculus, then run the machine's single-step function on the thread pool for P. If for some general evaluation context E the machine produces a state that is not equivalent to the thread pool for E[Q] after the same number of steps, adequacy fails and the machine-level soundness result cannot be transferred to the calculus; the paper's own properties modules already cover beta and pair reduction in all contexts, so the remaining general-context cases for close, wait, fork, and new are the ones to test.

Watch

Extended reading notes

Core claim

The central claim is that type preservation and session fidelity can be made definitional rather than derived. In the Agda formalization of the GV-style calculus, every value, environment, continuation, command, and thread pool is indexed by its type and session context, so the step function cannot produce an ill-typed state. Session fidelity is enforced by representing each channel as a resource whose session type changes by a context reduction on every communication, and by requiring the scheduler to find a matching partner for each close, wait, send, or receive before any transmission can occur. Progress is relative: the scheduler's step function returns Stuck exactly when no thread can take a step and no communication partner exists, giving a machine-checked account of deadlock situations. The formalization covers linear call-by-value PCF with pairs, forking, channel creation, closing, sending and receiving values, internal and external choice, recursive sessions with coinductive subtyping, and an encoding of asynchronous channels as chains of promise channels.

Load-bearing premise

The machine's step relation must faithfully mirror the calculus's own reduction rules in every evaluation context, and the author reports that the proof of this adequacy property for general contexts has not yet been completed.

Editorial extensions

If this is right

  • Any program accepted by the intrinsically typed syntax cannot fail by type confusion: a Stuck result from the scheduler indicates a true absence of matching communication partners, not an ill-typed state.
  • Session fidelity is maintained when channels are transmitted over other channels: the resource splitting tree moves the endpoint from sender to receiver, and the context reduction updates its session type accordingly.
  • The same machine, extended with choice, recursive sessions, and coinductive subtyping, still preserves typing by construction, so the approach scales beyond the minimal calculus.
  • The typed encoding of asynchronous channels as promise chains inherits type preservation and session fidelity from the synchronous machine.
  • Linearity is preserved throughout execution because the context splitting and resource splitting relations make it impossible to duplicate or discard a linear channel endpoint.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The resource splitting tree is essentially a separation-logic heap in disguise; making that connection explicit could simplify the rotation lemmas and may lead to more modular proofs for larger calculi.
  • Because structured gas lets the scheduler rotate the thread pool by arbitrary amounts, the same executable machine can explore every interleaving; that could support machine-checked deadlock-freedom or fairness statements for fragments of the calculus.
  • The promise-chain encoding of asynchrony suggests an executable asynchronous semantics can be obtained from the synchronous machine plus forked helper threads, so the framework could be tested by running asynchronous protocols against a directly asynchronous calculus.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents an Agda formalization of an intrinsically typed, executable small-step semantics for a functional session type calculus in the style of Gay and Vasconcelos. The core artifact is a multi-threaded CEK machine in which expressions, values, environments, continuations, and a global session context are all type-indexed, with linearity enforced by a context-splitting relation and a resource-splitting tree. The scheduler executes commands such as New, Close, Wait, Send, and Recv, and channel rendezvous is implemented by matching functions that carry equality and session-type-evolution proofs. The paper claims type preservation by construction, a notion of progress embodied in the scheduler's step function, and preliminary adequacy results relating the machine to a small-step semantics. It also sketches extensions for choice, recursive sessions, subtyping, structured gas, and an asynchronous encoding.

Significance. If the advertised claims were fully established, this would be a valuable mechanized semantics contribution: the resource-splitting tree is a genuinely useful technique for maintaining linearity and uniqueness of channel endpoints across threads, and the intrinsically typed CEK machine gives machine-checked type preservation for the machine-level semantics. The GitHub artifact and the honest discussion of what is and is not proved are strengths. However, the paper's central contribution as stated—'the first mechanized proof of type soundness and session fidelity of a realistic, fully-fledged functional session type calculus'—is not yet supported, because the adequacy bridge from the machine to the published calculus is incomplete and because the progress and session-fidelity claims are largely definitional rather than stated as proved theorems.

major comments (3)
  1. [§5.4, Adequacy] The paper's advertised type-soundness claim is for the GV-style calculus, but the machine-checked results are for the CEK machine. Section 5.4 explicitly states: 'Adequacy does not follow from the intrinsic typedness of the interpreter, but requires separate proofs' and that the proofs 'for general contexts get very complex and we have not been able to complete them.' The only completed adequacy results are for beta and pair reductions in simple contexts plus close/wait/fork/new in very simple contexts. Without a general-context adequacy theorem, a statement about start and schedule gas is a theorem about the machine, not about the expression/process calculus of Figs. 3 and 24. The central claim of calculus-level type soundness therefore overstates what is proved.
  2. [§7, Conclusions; §4.5, Scheduler] The progress claim is close to definitional. The conclusion asserts that when the step function returns Stuck, 'all remaining communication commands do not have a corresponding partner at the other end of the channel,' but this is an interpretation of the implementation of step, matchWaitAndGo, and the vcr-match functions, not a proved completeness property. In particular, there is no theorem stating that Stuck occurs exactly when no thread can make a step and no matching communication partner exists; the code simply produces Stuck when its matching routines return nothing. Thus the paper's 'relative progress by construction' is a design property of the scheduler, not a metatheorem about the calculus.
  3. [Abstract, §1, and Section 5.3-5.4] The paper claims a 'first fully mechanized proof of session fidelity,' but no standalone session fidelity theorem is stated or proved. The matching functions such as vcr-match-2-sr include equality proofs (e.g., t1 ≡ t2 and dual s1 ≡ s2) that establish compatibility of matched channel ends, and type preservation of the machine ensures that channel types evolve consistently. However, session fidelity as a property of the calculus—that every communication step in every run follows the stated protocol—is never formulated as a theorem. The authors should either state and prove such a theorem at the machine level and connect it via adequacy to the calculus, or explicitly qualify the session-fidelity claim.
minor comments (4)
  1. [§1, Introduction] There are typos: 'sychronous' should be 'synchronous' and 'asychronous' should be 'asynchronous' in the bullet list; also the Agda pattern synonym syntax appears as 'pa/t_tern' in several places, which looks like a rendering artifact and should be fixed.
  2. [§4.5, Figure 13] The type constructor '_,_' : Event → Outcome → Outcome is used to package an event with an outcome, but the notation is easy to confuse with a pair type in Agda. A named record or a comment explaining this constructor would improve readability.
  3. [§5.4, Adequacy] The modules Properties.StepBeta and Properties.StepPair are mentioned but their exact statements are not reproduced. Since these are the main adequacy results, the paper should state at least the theorem statements in prose or as displayed equations so that the reader can verify what has actually been shown.
  4. [§6, Related Work] The comparison with Goto et al. [2016] focuses on representation style, but it does not clearly state whether Goto et al.'s 'safety properties' include session fidelity or only subject reduction and deadlock-freedom-like properties. This makes it difficult to assess the novelty of the claimed first session-fidelity proof.

Circularity Check

1 steps flagged · score 6.0 of 10

Relative progress is defined as the step function's failure case, and the adequacy bridge from the CEK machine to the GV-style calculus is explicitly left incomplete; the advertised calculus-level type soundness is therefore partly circular and partly unproven.

  1. self definitional [Section 7 (Conclusions), progress claim; cf. Section 4.5 scheduler step function]
    "Progress is embodied in the definition of the step function (Section 4.5). By design, this function returns Stuck, if it cannot make progress. That is, there is no command in the thread pool that can execute immediately and all remaining communication commands do not have a corresponding partner at the other end of the channel. Stating such a relative progress result feels like a futile exercise because its definition and proof mirror exactly the definitions of step, the match*AndGo functions, and the vcr-match* functions."

    The paper's central soundness claim includes this 'relative progress' component, but the property is true by construction: Stuck is the event emitted by the step function exactly when it cannot take a step, and the paper itself says a proof would mirror the step/match definitions. There is no independent 'cannot make progress' predicate being verified; the theorem is the failure case of the implementation, so the progress 'result' reduces to the definition of step. The deadlock interpretation is likewise definitional: Section 4.5 says the configuration 'indicates a deadlock because the step function was not able to execute any command in the thread pool.' Type preservation remains a genuine Agda-checked property, but the soundness claim as a whole is partly tautological.

full rationale

The Agda formalization is a substantial, machine-checked development: type preservation, linearity, and resource-splitting invariants are enforced by the intrinsically typed representation, and no load-bearing self-citation or imported uniqueness theorem occurs. However, the headline contribution as stated in the introduction—'the first mechanized proof of the type soundness and session fidelity of a realistic, fully-fledged functional session type calculus'—outruns what the paper establishes. First, the progress half of type soundness is self-definitional: Section 7 states that progress is embodied in the step function and that a proof would mirror the definitions of step, match*AndGo, and vcr-match*, so the property is the step function's failure case by construction. Second, the bridge from the machine to the published calculus is explicitly incomplete: Section 5.4 says 'Adequacy does not follow from the intrinsic typedness of the interpreter, but requires separate proofs' and that the proofs for general contexts 'get very complex and we have not been able to complete them.' Consequently, the machine-level preservation and matching results are not yet theorems about the GV-style process calculus of Figures 3 and 24. Session fidelity, as an advertised calculus property, inherits the same adequacy gap; within the machine it is enforced by the return types of vcr-match functions rather than derived for an independently specified reduction relation. These are internal, textually acknowledged limitations, and the definitional progress step is the concrete circular component. Overall, the central formalization has substantial independent content, but the paper's soundness/fidelity headline is partially circular (progress) and partially unproven (adequacy), warranting a score of 6 rather than a lower or higher value.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No fitted constants or ad hoc mathematical objects are introduced; the resource splitting tree, ChannelRef, Command, and promise-channel encoding are modeling constructs defined in the paper, not postulated entities with independent empirical content. The trust assumptions are Agda itself and the adequacy of the machine to a reference semantics.

assumptions (3)
  • standard math Agda's type theory, termination checking, and standard library are sound.
    The formalization relies on Agda's type checker and library predicates such as Data.List.All and Data.Fin; no separate proof of the consistency of this trusted core is provided.
  • domain assumption Coinductive session types and coinductive subtyping represent recursive sessions and match the intended greatest-fixpoint semantics.
    Sections 5.2 and A.4 define SType and Sub as coinductive records; the paper assumes productivity and the correspondence to recursive session types.
  • domain assumption The GV-style process calculus is the intended reference semantics and the CEK machine adequately implements it.
    The paper calls MicroSession a subset of Gay and Vasconcelos [2010] and uses that calculus as the target, but adequacy is only partially proved in Section 5.4.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Intrinsically-Typed Mechanized Semantics for Session Types." pith.science (2026). https://pith.science/paper/27T4U5RN

@misc{pith2026190802940,
  author       = {Pith},
  title        = {Pith review of: Intrinsically-Typed Mechanized Semantics for Session Types},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/27T4U5RN}},
  note         = {Machine review of arXiv:1908.02940}
}
read the original abstract

Session types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages with session types are tedious and technically involved, it is rare to see mechanized soundness proofs for these systems. We present an executable intrinsically typed small-step semantics for a realistic functional session type calculus. The calculus includes linearity, recursion, and recursive sessions with subtyping. Asynchronous communication is modeled with an encoding. The semantics is implemented in Agda as an intrinsically typed, interruptible CEK machine. This implementation proves type preservation and a particular notion of progress by construction.

Figures

Figures reproduced from arXiv: 1908.02940 by the authors.

Figure 1
Figure 1. Session types, types, and typing contexts [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Unrestricted types and context splitting [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 4
Figure 4. Duality lemma dual-inv : ∀ s → dual (dual s) ≡ s. 2 [PITH_FULL_IMAGE:figures/full_fig_p003_4.png] view at source ↗
Figures from the paper (20 more)
Figure 3
Figure 3. Figure 3: Expression typing [PITH_FULL_IMAGE:figures/full_fig_p003_3.png]
Figure 5
Figure 5. Figure 5: Example term Variables (var) are represented by de Bruijn indices into the con￾text. Accessing variables is formalized in the type t ∈ Φ, which im￾plements weakening only for unrestricted variables. If the variable is on top of the context (constructor here), then all …
Figure 7
Figure 7. Figure 7: Resource splitting for threads G which makes available exactly the resources used by this en￾tity. These semantic entities are (in order of containment) (1) the thread pool (i.e., a process in normal form), (2) expression threads, (3) value environments, (4) values. It…
Figure 8
Figure 8. Figure 8: Resource splitting G G1 G11 G12 G2 (a) Before G G11 Gi G12 G2 (b) After [PITH_FULL_IMAGE:figures/full_fig_p006_8.png]
Figure 9
Figure 9. Figure 9: Action of ssplit-compose ssplit-compose : {G G1 G2 G11 G12 : SCtx} → SSplit G G1 G2 → SSplit G1 G11 G12 → Σ SCtx λ Gi → SSplit G G11 Gi × SSplit Gi G12 G2 It transforms the splitting tree in Figure 9a to the one in Figure 9b, highlighting the new intermediate session c…
Figure 12
Figure 12. Figure 12: Continuations / Evaluation contexts (channel ends). The refinement arises because the typing environ￾ment manages variable bindings, whereas the session context keeps track of single resources. One part of the resources (indexed by G1) is referenced in the en￾vironmen…
Figure 13
Figure 13. Figure 13: Auxiliary types for the scheduler The Fork command contains two continuations (thunks, really), one for the newly created thread and the other for continuing the existing thread. The scheduler applies each thunk to the unit value. Its construction in decompose is a te…
Figure 16
Figure 16. Figure 16: Stepping — the New command ... | Stuck , _ , tp′ = Stuck ... | ev , _ , tp′ = ev , schedule gas tp′ The scheduler repeatedly applies the single-step function to a thread pool. At this point we cannot easily predict termination, so the scheduler runs on a provided supp…
Figure 15
Figure 15. Figure 15: First steps current thread pool as the first argument and an empty pool as the second. The step function considers commands from the first list and either executes them or moves them to the second list. In the first case for step, both lists are empty and the program …
Figure 17
Figure 17. Figure 17: Stepping — the Wait command step ss-top (tcons{G1}{G2} ss cmd@(Close ss-vϰ v ϰ) tp) tp2 with ssplit-compose ss-top ss ... | Gi , ss-top1 , ss-top2 with ssplit-refl-le -inactive Gi ... | G ′ , ina-G′ , ss-GG′ with matchWaitAndGo ss-top1 (ss-vϰ , v , ϰ) ss-GG′ (tappend …
Figure 18
Figure 18. Figure 18: Stepping — the Close command vcr-match ss-[] () vcr2 vcr-match (ss-both ss) (there vcr1) (there vcr2) = map (λ{ (b≡ , G ′ , R , ina) → (b≡ , nothing :: G ′ , RedThere R , ina-:: G ′ ina) }) (vcr-match ss vcr1 vcr2) vcr-match (ss-le ss) vcr1 (there vcr2) = nothing vcr-…
Figure 19
Figure 19. Figure 19: Implementation of vcr-match values, and resource splittings. This weakening is straightforward because we chose to expose all values in a thread in traversable data types. Weakening is implemented by the li functions. 4.7 Close and Wait A waiting thread just stays in …
Figure 20
Figure 20. Figure 20: Commands for sending and receiving vcr-match-2-sr : ∀ {G G1 G2 G11 G12 b1 b2 s1 s2 t1 t2} → Junction G G1 G2 G11 G12 → ValidChannelRef G11 b1 (SRecv t1 s1) → ValidChannelRef G12 b2 (SSend t2 s2) → Maybe (b1 ≡ otherEnd b2 × t1 ≡ t2 × dual s1 ≡ s2 × ∃ λ G ′ → ∃ λ G1 ′ →…
Figure 21
Figure 21. Figure 21: Matching channel ends for sending and receiving [PITH_FULL_IMAGE:figures/full_fig_p011_21.png]
Figure 22
Figure 22. Figure 22: Splitting and changing the resource state [PITH_FULL_IMAGE:figures/full_fig_p011_22.png]
Figure 23
Figure 23. Figure 23: Resource transfer. Updated splittings are highl [PITH_FULL_IMAGE:figures/full_fig_p012_23.png]
Figure 25
Figure 25. Figure 25: Splitting among values llambda : ∀ {t1 t2} → (body : Expr (t1 :: Φ) t2) → Expr Φ (TFun LL t1 t2) rec : ∀ {t1 t2} → (unr-Φ : All Unr Φ) → let t = TFun UU t1 t2 in (body : Expr (t :: t1 :: Φ) t2) → Expr Φ t app : ∀ {Φ1 Φ2 lu t1 t2} → (sp : Φ , Φ1 ◦ Φ2) → (fun : TFun lu …
Figure 26
Figure 26. Figure 26: Expressions for function types A.3 Functions and Recursion The extension with functions and recursion is standard, except for dealing with linearity [PITH_FULL_IMAGE:figures/full_fig_p016_26.png]
Figure 27
Figure 27. Figure 27: Recursive sessions mutual -- subtyping data SubT : Type → Type → Set where sub-unit : SubT TUnit TUnit sub-pair : ∀ {t1 t2 t1 ′ t2 ′ } → SubT t1 t1 ′ → SubT t2 t2 ′ → SubT (TPair t1 t2) (TPair t1 ′ t2 ′ ) sub-fun : ∀ {t1 t2 t1 ′ t2 ′ lu} → SubT t1 ′ t1 → SubT t2 t2 ′ …
Figure 28
Figure 28. Figure 28: Subtyping of recursive session types types. All nontrivial subtyping is generated by the two construc￾tors / rules sub-sint and sub-sext corresponding to internal and external choice. For the internal choice, the supertype has fewer alternatives m′ ≤ m. The premises o…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

20 extracted references · 18 canonical work pages

  1. [1]

    2017.Interactive Programming in Agda - Objects and Graphical User Interfaces

    Andreas Abel, Stephan Adelsberger, and Anton Setzer. 2017.Interactive Programming in Agda - Objects and Graphical User Interfaces. J. Funct. Program. 27 (2017), e8. Guillaume Allais, James Chapman, Conor McBride, and James M cKinna

    work page 2017

  2. [2]

    Pair Channel Int Channel Figure 25: Splitting among values llambda : ∀ {t1 t2} → (body : Expr (t1 :: Φ) t2) → Expr Φ (TFun LL t1 t2) rec : ∀ {t1 t2} → (unr-Φ : All Unr Φ) → let t = TFun UU t1 t2 in (body : Expr (t :: t1 :: Φ) t2) → Expr Φ t app : ∀ {Φ1 Φ2 lu t1 t2} → (sp : Φ ≜Φ1 ◦ Φ2) → (fun : TFun lu t1 t2 ∈ Φ1) → (arg : t1 ∈ Φ2) → Expr Φ t2 Figure 26: E...

    work page 2018

  3. [7]

    Objects and Session Types. Inf. Comput. 207, 5 (2009), 595–641. Matthias Felleisen and Daniel Friedman

    work page 2009

  4. [8]

    Acta Informatica 42, 2-3 (2005), 191–225

    Subtyping for Session Ty pes in the Pi Calculus. Acta Informatica 42, 2-3 (2005), 191–225. Simon J. Gay and Vasco Thudichum Vasconcelos

    work page 2005

  5. [11]

    ACM Comput

    Foundat ions of Session Types and Behavioural Contracts. ACM Comput. Surv. 49, 1 (2016), 3:1–3:36. Sam Lindley and J. Garrett Morris

    work page 2016

  6. [14]

    Mathematical Structures in Computer Science 28, 9 (2018), 1541–1577

    Proof-relevant π -calculus: a constructive ac- count of concurrency and causality. Mathematical Structures in Computer Science 28, 9 (2018), 1541–1577. https://doi.org/10.1017/S09601 2951700010X Benjamin C. Pierce and Davide Sangiorgi

    work page doi:10.1017/s09601 2018

  7. [15]

    PACMPL 2, POPL (2018), 16:1–16:34

    Intrinsically-typed Definitional Interpret ers for Imperative Lan- guages. PACMPL 2, POPL (2018), 16:1–16:34. John C. Reynolds

    work page 2018

  8. [17]

    Context-fre e session types. In Proceedings of the 21st ACM SIGPLAN International Conference on Func- tional Programming, ICFP 2016, Nara, Japan, September 18-22 , 2016 , Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, Na ra, Japan, 462–475. https://doi.org/10.1145/2951913.2951926 Bernardo Toninho, Luís Caires, and Frank Pfenning

    arXiv 2016

Show all 20 references
  1. [18]

    Woodstock ’18, June 03–05, 2018, Woodstock, NY Peter Thiemann A SUPPLEMENTARY MATERIAL A.1 Processes data Proc Φ : Set where exp : (e : Expr Φ TUnit) → Proc Φ par : ∀ {Φ1 Φ2} → (sp : Split Φ Φ1 Φ2) → (P1 : Proc Φ1) → (P2 : Proc Φ2) → Proc Φ res : (s : STy) → (P : Proc (TChan s...

    2018

  2. [24]

    This context only contains bindings for channel endpoints

    Processes are also intri nsically typed and hence indexed by a typing context Φ. This context only contains bindings for channel endpoints. A process P is either an expression process ( exp), a parallel execution of processes ( par) which splits the environment for its two sub...

    2005

  3. [203]

    https://doi.org/10.4204/EPTCS.203.1 Scott Owens, Magnus O

    1–13. https://doi.org/10.4204/EPTCS.203.1 Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Ta n

    doi

  4. [2001]

    ACM TOPLAS 23, 5 (2001), 657–683

    An Indexed Mod el of Recursive Types for Foundational Proof-Carrying Code. ACM TOPLAS 23, 5 (2001), 657–683. https://doi.org/10.1145/504709.504712 Robert Atkey

    2001

  5. [2005]

    Logical Methods in Computer Science 1, 2 (2005)

    General Recursion via Coinductiv e Types. Logical Methods in Computer Science 1, 2 (2005). Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elen a Giachino, and Luca Padovani

    2005

  6. [2009]

    In Principles and Practice of Declara- tive Programming, PPDP 2009, António Porto and Francisco J

    Foundations of Session Types. In Principles and Practice of Declara- tive Programming, PPDP 2009, António Porto and Francisco J. López-Fraguas (Eds.). ACM, Coimbra, Portugal, 219–230. Iliano Cervesato and Frank Pfenning

    2009

  7. [2010]

    Linear Type Theory for Asyn- chronous Session Types. J. Funct. Program. 20, 1 (2010), 19–50. Matthew A. Goto, Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, and James Riely

    2010

  8. [2012]

    Strongly Typed Term Representations in Coq. J. Autom. Reasoning 49, 2 (2012), 141–159. Luís Caires and Frank Pfenning

    2012

  9. [2013]

    http://siek.blogspot.de/2013/05/type-safety-in-thre e-easy-lemmas.html

    Type Safety in Three Easy Lemmas. http://siek.blogspot.de/2013/05/type-safety-in-thre e-easy-lemmas.html. (May 2013). Peter Thiemann and Vasco T. Vasconcelos

    2013

  10. [2015]

    In Proceedings Eighth International Workshop on Programming La nguage Ap- proaches to Concurrency- and Communication-cEntric Softw are, PLACES 2015, Lon- don, UK, 18th April

    Using Session Types as an Effect Sys- tem. In Proceedings Eighth International Workshop on Programming La nguage Ap- proaches to Concurrency- and Communication-cEntric Softw are, PLACES 2015, Lon- don, UK, 18th April

    2015

  11. [2016]

    Mathematical Structures in Computer Science 26, 3 (2016), 465–509

    An Extensible Approach to Session Polymorphism. Mathematical Structures in Computer Science 26, 3 (2016), 465–509. Kohei Honda

    2016

  12. [2018]

    Au- tomated Modular Verification for Relaxed Communication Pro tocols. In Pro- gramming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings (L ecture Notes in Computer Science) , Sukyoung Ryu (Ed.), Vol. 11275. Spri...

    2018 doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.