Programming interfaces and basic topology

DOI10.1016/J.APAL.2005.05.022MaRDI QIDQ2575770zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 6 December 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.022

zbMATH Keywords

Constructive type theoryFormal topologyPredicate transformersSimulation

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Categorical semantics of formal languages (18C50) Topological spaces and generalizations (closure spaces, etc.) (54A05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Types for Proofs and Programs
• scientific article; zbMATH DE number 910713
• Structured Co-spans: An Algebra of Interaction Protocols
• scientific article; zbMATH DE number 860038
• scientific article; zbMATH DE number 3958777

Cites work

• A semantics of evidence for classical arithmetic
• A set constructor for inductive sets in Martin-Löf's type theory
• A single complete rule for data refinement
• An axiomatic basis for computer programming
• Computer Science Logic
• Defining liveness
• Encoding, decoding and data refinement
• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 4152376 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 4035828 (Why is no real title available?)
• scientific article; zbMATH DE number 41225 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 3628353 (Why is no real title available?)
• scientific article; zbMATH DE number 1302065 (Why is no real title available?)
• scientific article; zbMATH DE number 952103 (Why is no real title available?)
• scientific article; zbMATH DE number 1420795 (Why is no real title available?)
• scientific article; zbMATH DE number 3212008 (Why is no real title available?)
• scientific article; zbMATH DE number 2247254 (Why is no real title available?)
• Inductively generated formal topologies.
• Proving the Correctness of Multiprocess Programs
• Refinement Calculus
• Some points in formal topology.
• State dependent IO-monads in type theory
• The existence of refinement mappings
• The point of pointless topology
• The problem of the formalization of constructive topology

Cited in

(9)

• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• From proposition to program. Embedding the refinement calculus in Coq
• A minimalist foundation at work
• scientific article; zbMATH DE number 3958777 (Why is no real title available?)
• Doo bee doo bee doo
• Representing continuous functions between greatest fixed points of indexed containers
• Indexed containers
• Interactive programming in Agda -- objects and graphical user interfaces
• A linear category of polynomial diagrams

This page was built for publication: Programming interfaces and basic topology

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