Algebra of Programming Using Dependent Types

DOI10.1007/978-3-540-70594-9_15zbMATH Open1156.68358OpenAlexW1575779505MaRDI QIDQ3521992FDOQ3521992

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

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

Mathematics Subject Classification ID

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

Cites Work

• Inductive families
• Dependent ML An approach to practical programming with dependent types
• Title not available (Why is that?)
• The view from the left
• Higher-order matching for program transformation
• Functional algorithm design
• Cayenne -- a language with dependent types
• Relational and Kleene-Algebraic Methods in Computer Science

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)