Algebra of Programming Using Dependent Types

DOI10.1007/978-3-540-70594-9_15MaRDI QIDQ3521992zbMATHOpenAlexFDO

Authors Shin-Cheng Mu, Hsiang-Shang Ko, Patrik Jansson

Publication date 28 August 2008

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

Full work available at URL https://doi.org/10.1007/978-3-540-70594-9_15

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Programming and reasoning with algebraic effects and dependent types
• Dependent types in mathematical theory of programming
• Algebra of programming in Agda: Dependent types for relational program derivation
• Dependent types and program equivalence
• An algorithm for type-checking dependent types
• Dependent types and formal synthesis
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 3970091
• Algebraic structures as typed objects
• Reasoning about algebraic data types with abstractions

Cites work

• scientific article; zbMATH DE number 977284 (Why is no real title available?)
• Cayenne -- a language with dependent types
• Dependent ML An approach to practical programming with dependent types
• Functional algorithm design
• Higher-order matching for program transformation
• Inductive families
• Relational and Kleene-Algebraic Methods in Computer Science
• The view from the left

Cited in

(3)

• Type directed compilation of row-typed algebraic effects
• Algebra of programming in Agda: Dependent types for relational program derivation
• Dependent types in mathematical theory of programming

This page was built for publication: Algebra of Programming Using Dependent Types

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