Interactive programs in dependent type theory

DOI10.1007/3-540-44622-2_21MaRDI QIDQ2753682zbMATH OpenFDO

Authors Peter Hancock, Anton Setzer

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44622-2_21

zbMATH Keywords

dependent typesfunctional programminginteractionmonadic I/Oreactive programmingrefinementrepetition constructs

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2247254
• State dependent IO-monads in type theory
• Interactive programming in Agda -- objects and graphical user interfaces
• Types for Proofs and Programs
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory

Cited in

(24)

• Undecidability of equality for codata types
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• Programming interfaces and basic topology
• Continuity of Gödel's system T definable functionals via effectful forcing
• Computation by interaction for space-bounded functional programming
• From proposition to program. Embedding the refinement calculus in Coq
• Dependent types and fibred computational effects
• The coinductive resumption monad
• State dependent IO-monads in type theory
• Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
• Dependently Typed Programming Based on Automated Theorem Proving
• Ludics with repetitions (Exponentials, Interactive types and Completeness)
• Data types with symmetries and polynomial functors over groupoids
• How to reason coinductively informally
• Flag-based big-step semantics
• Coalgebras as types determined by their elimination rules
• Interactive programming in Agda -- objects and graphical user interfaces
• No value restriction is needed for algebraic effects and handlers
• Idris, a general-purpose dependently typed programming language: Design and implementation
• scientific article; zbMATH DE number 2247254 (Why is no real title available?)
• Types for Proofs and Programs
• Hefty algebras: modular elaboration of higher-order effects
• Defining trace semantics for CSP-Agda
• Oracle modalities

This page was built for publication: Interactive programs in dependent type theory

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