Dependently-Typed Formalisation of Relation-Algebraic Abstractions

DOI10.1007/978-3-642-21070-9_18zbMath1329.68063OpenAlexW23023570MaRDI QIDQ3007580

Wolfram Kahl

Publication date: 17 June 2011

Published in: Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21070-9_18

zbMATH Keywords

dependently typed programmingnested algebrasalgebras as dataallegories of relational algebra morphisms

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Related Items

Towards Certifiable Implementation of Graph Transformation via Relation Categories ⋮ Typing theorems of omega algebra ⋮ Towards ``mouldable code via nested code graph transformation ⋮ Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck} ⋮ Cardinalities of Finite Relations in Coq ⋮ Formalization of universal algebra in Agda

Uses Software

• Isabelle/Isar
• Haskell
• Prover9
• Agda