CHoCO

This is a list of references on the Curry-Howard correspondences for Concurrency (CHoCo), which I have constructed with the help of DBLP. The list is not exhaustive, and is mainly intended for my own reference. Still, I thought it may be of interest also to others, hence this page.

Please contact me if you have suggestions of any kind; in particular, there may be relevant works that are not listed here.

(Photo credit: Pixabay)

Introductory Papers

  • Philip Wadler: Propositions as types. Commun. ACM 58(12): 75-84 (2015) [DOI]
  • Luís Caires, Frank Pfenning, Bernardo Toninho: Towards concurrent type theory. TLDI 2012: 1-12 [DOI]
  • Samson Abramsky: Proofs as Processes. Theor. Comput. Sci. 135(1): 5-9 (1994) [DOI]

Developments Since 2010

  • Robert Atkey: Observed Communication Semantics for Classical Processes. ESOP 2017: 56-82 [DOI]
  • Stephanie Balzer, Frank Pfenning: Manifest Sharing with Session Types. ICFP 2017: 37 [DOI]
  • Luís Caires, Jorge A. Pérez. Linearity, Control Effects, and Behavioral Types. ESOP 2017: 229-259 [DOI]
  • Marco Carbone, Fabrizio Montesi, Carsten Schürmann, Nobuko Yoshida: Multiparty session types as coherence proofs. Acta Inf. 54(3): 243-269 (2017) [DOI]
  • Cosku Acay, Frank Pfenning: Intersections and Unions of Session Types. ITRS 2016: 4-19 [DOI]
  • Robert Atkey, Sam Lindley, J. Garrett Morris: Conflation Confers Concurrency. A List of Successes That Can Change the World 2016: 32-55 [DOI]
  • Luís Caires, Frank Pfenning, Bernardo Toninho: Linear logic propositions as session types. Mathematical Structures in Computer Science 26(3): 367-423 (2016) [DOI]
  • Luís Caires, Jorge A. Pérez: Multiparty Session Types Within a Canonical Binary Theory, and Beyond. FORTE 2016: 74-95 [DOI]
  • Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, Philip Wadler: Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. CONCUR 2016: 33:1-33:15 [DOI]
  • Limin Jia, Hannah Gommerstadt, Frank Pfenning: Monitors and blame assignment for higher-order session types. POPL 2016: 582-594 [DOI]
  • Sam Lindley, J. Garrett Morris: Talking bananas: structural recursion for session types. ICFP 2016: 434-447 [DOI]
  • Stephanie Balzer, Frank Pfenning: Objects as session-typed processes. AGERE!@SPLASH 2015: 13-24 [DOI]
  • Marco Carbone, Fabrizio Montesi, Carsten Schürmann, Nobuko Yoshida: Multiparty Session Types as Coherence Proofs. CONCUR 2015: 412-426 [DOI]
  • Ornela Dardha, Jorge A. Pérez: Comparing Deadlock-Free Session Typed Processes. EXPRESS/SOS 2015: 1-15 [DOI]
  • Sam Lindley, J. Garrett Morris: A Semantics for Propositions as Sessions. ESOP 2015: 560-584 [DOI]
  • Frank Pfenning, Dennis Griffith: Polarized Substructural Session Types. FoSSaCS 2015: 3-22 [DOI]
  • Marco Carbone, Fabrizio Montesi, Carsten Schürmann: Choreographies, Logically. CONCUR 2014: 47-62 [DOI]
  • Sam Lindley, J. Garrett Morris: Sessions as Propositions. PLACES 2014: 9-16 [DOI]
  • Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho: Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput. 239: 254-302 (2014) [DOI]
  • Bernardo Toninho, Luís Caires, Frank Pfenning: Corecursion and Non-divergence in Session-Typed Processes. TGC 2014: 159-175 [DOI]
  • Philip Wadler: Propositions as sessions. J. Funct. Program. 24(2-3): 384-418 (2014) [DOI]
  • Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho: Behavioral Polymorphism and Parametricity in Session-Based Communication. ESOP 2013: 330-349 [DOI]
  • Bernardo Toninho, Luís Caires, Frank Pfenning: Higher-Order Processes, Functions, and Sessions: A Monadic Integration. ESOP 2013: 350-369 [DOI]
  • Henry DeYoung, Luís Caires, Frank Pfenning, Bernardo Toninho: Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. CSL 2012: 228-242 [DOI]
  • Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho: Linear Logical Relations for Session-Based Concurrency. ESOP 2012: 539-558 [DOI]
  • Bernardo Toninho, Luís Caires, Frank Pfenning: Functions as Session-Typed Processes. FoSSaCS 2012: 346-360 [DOI]
  • Philip Wadler: Propositions as sessions. ICFP 2012: 273-286 [DOI]
  • Frank Pfenning, Luís Caires, Bernardo Toninho: Proof-Carrying Code in a Session-Typed Process Calculus. CPP 2011: 21-36 [DOI]
  • Bernardo Toninho, Luís Caires, Frank Pfenning: Dependent session types via intuitionistic linear type theory. PPDP 2011: 161-172 [DOI]
  • Luís Caires, Frank Pfenning: Session Types as Intuitionistic Linear Propositions. CONCUR 2010: 222-236 [DOI]

Developments Prior to 2010

  • Gianluigi Bellin, Philip J. Scott: On the pi-Calculus and Linear Logic. Theor. Comput. Sci. 135(1): 11-65 (1994) [DOI]
  • Samson Abramsky: Computational Interpretations of Linear Logic. Theor. Comput. Sci. 111(1&2): 3-57 (1993) [DOI]