Defining trace semantics for CSP-Agda

DOI10.4230/LIPICS.TYPES.2016.12MaRDI QIDQ6855245zbMATH OpenFDO

Authors Bashar Igried, Anton Setzer

Publication date 20 February 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2016.12

zbMATH Keywords

Agdacoalgebrascoinductive data typesCSPdependent type theoryinduction-recursioninteractive programIO-monadmonadmonadic programmingprocess algebrassized typestrace semanticsuniverses

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• A Brief Overview of Agda – A Functional Language with Dependent Types
• A general formulation of simultaneous inductive-recursive definitions in type theory
• A light-weight integration of automated and interactive theorem proving
• Communicating sequential processes
• Compositional coinduction with sized types
• Copatterns, programming infinite structures by observations
• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• Induction-recursion and initial algebras.
• Infinite objects in type theory
• Interactive programming in Agda -- objects and graphical user interfaces
• Notions of computation and monads
• Unnesting of copatterns

This page was built for publication: Defining trace semantics for CSP-Agda

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