Proof-carrying code in a session-typed process calculus

DOI10.1007/978-3-642-25379-9_4MaRDI QIDQ3100198zbMATH OpenOpenAlexFDO

Authors Luís Caires, Bernardo Toninho, Frank Pfenning

Publication date 22 November 2011

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-25379-9_4

zbMATH Keywords

process calculusproof irrelevanceproof-carrying codesession types

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Depending on session-typed processes
• Session types revisited
• Session types as generic process types
• CONCUR 2004 - Concurrency Theory
• Subtyping for session types in the pi calculus

Cites work

• Correspondence assertions for process synchronization in concurrent communications
• scientific article; zbMATH DE number 1398002 (Why is no real title available?)
• Lolliproc: to concurrency from classical linear logic via Curry-Howard and control
• Proof-carrying code in a session-typed process calculus
• Propositions as [Types]
• Secure distributed programming with value-dependent types
• Session types as intuitionistic linear propositions

Cited in

(22)

• Depending on session-typed processes
• Process calculi as a tool for studying coordination, contracts and session types
• Certifying data in multiparty session types
• Fairness and communication-based semantics for session-typed languages
• Event structure semantics for multiparty sessions
• Corecursion and non-divergence in session-typed processes
• On session types and polynomial time
• Observed Communication Semantics for Classical Processes
• Linearity, control effects, and behavioral types
• Proof-carrying code in a session-typed process calculus
• I got plenty o' nuttin'
• Certifying data in multiparty session types
• Linear logical relations and observational equivalences for session-based concurrency
• scientific article; zbMATH DE number 7453964 (Why is no real title available?)
• Session Types with Arithmetic Refinements
• Domain-aware session types
• Relating Process Languages for Security and Communication Correctness (Extended Abstract)
• The different shades of infinite session types
• System \(F^\mu_\omega\) with context-free session types
• Safe session-based concurrency with shared linear state
• Object-level reasoning with logics encoded in HOL Light
• Combining behavioural types with security analysis

Describes a project that uses

Uses Software

• Lolliproc
• F*

This page was built for publication: Proof-carrying code in a session-typed process calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100198)