Algebra of programming in Agda: Dependent types for relational program derivation

DOI10.1017/S0956796809007345zbMath1191.68195WikidataQ114849894 ScholiaQ114849894MaRDI QIDQ3644935

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

Publication date: 13 November 2009

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

terminating hylomorphisms

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Theory of software (68N99)

Related Items (9)

Unnamed Item ⋮ Formal derivation of greedy algorithms from relational specifications: a tutorial ⋮ Towards Certifiable Implementation of Graph Transformation via Relation Categories ⋮ Contributions to a computational theory of policy advice and avoidability ⋮ Calculating Certified Compilers for Non-deterministic Languages ⋮ Trends in trends in functional programming 1999/2000 versus 2007/2008 ⋮ Calculating a linear-time solution to the densest-segment problem ⋮ Program Calculation in Coq ⋮ Extensional equality preservation and verified generic programming

Uses Software

• Coq
• ALF
• Cayenne
• Agda
• AoPA

Cites Work

• Deforestation: Transforming programs to eliminate trees
• Terminating general recursion
• Type checking with universes
• Inductive families
• Theory and applications of inverting functions as folds
• Functional algorithm design
• Reductivity
• A lattice-theoretical fixpoint theorem and its applications
• Algebra of Programming Using Dependent Types
• The view from the left
• Dependent ML An approach to practical programming with dependent types
• Cayenne—a language with dependent types
• Proving Properties of Programs by Structural Induction
• Modelling general recursion in type theory
• Eliminating Dependent Pattern Matching

This page was built for publication: Algebra of programming in Agda: Dependent types for relational program derivation