State dependent IO-monads in type theory

MaRDI QIDQ2849882zbMATH OpenFDO

Authors Anton Setzer, Markus Michelbrink

Publication date 20 September 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105000368

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 2247254
• scientific article; zbMATH DE number 1670486
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• Interactive programming in Agda -- objects and graphical user interfaces
• Monads for behaviour

Cited in

(9)

• From global to local state, coalgebraically and compositionally
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• Programming interfaces and basic topology
• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
• The lax braided structure of streaming I/O
• Interactive programming in Agda -- objects and graphical user interfaces
• scientific article; zbMATH DE number 2247254 (Why is no real title available?)
• Types for Proofs and Programs

Describes a project that uses

Uses Software

• Agda

This page was built for publication: State dependent IO-monads in type theory

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