Proof-Carrying Code in a Session-Typed Process Calculus

DOI10.1007/978-3-642-25379-9_4zbMath1350.68204OpenAlexW1886109164MaRDI QIDQ3100198

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

session typesprocess calculusproof-carrying codeproof irrelevance

Mathematics Subject Classification ID

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

Related Items (17)

Relating Process Languages for Security and Communication Correctness (Extended Abstract) ⋮ Certifying data in multiparty session types ⋮ I Got Plenty o’ Nuttin’ ⋮ Certifying Data in Multiparty Session Types ⋮ Fairness and communication-based semantics for session-typed languages ⋮ Combining behavioural types with security analysis ⋮ Event structure semantics for multiparty sessions ⋮ The different shades of infinite session types ⋮ Unnamed Item ⋮ On session types and polynomial time ⋮ Unnamed Item ⋮ Observed Communication Semantics for Classical Processes ⋮ Linearity, Control Effects, and Behavioral Types ⋮ Linear logical relations and observational equivalences for session-based concurrency ⋮ Corecursion and Non-divergence in Session-Typed Processes ⋮ Session Types with Arithmetic Refinements ⋮ Proof-Carrying Code in a Session-Typed Process Calculus

Uses Software

• Lolliproc
• F*

Cites Work

• Proof-Carrying Code in a Session-Typed Process Calculus
• Session Types as Intuitionistic Linear Propositions
• Correspondence assertions for process synchronization in concurrent communications
• Propositions as [Types]
• Lolliproc
• Secure distributed programming with value-dependent types
• Unnamed Item

This page was built for publication: Proof-Carrying Code in a Session-Typed Process Calculus