Computing in Coq with Infinite Algebraic Data Structures

DOI10.1007/978-3-642-14128-7_18zbMath1286.68396OpenAlexW2951390372MaRDI QIDQ3582708

César Domínguez, Julio Jesús Rubio García

Publication date: 24 August 2010

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

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

zbMATH Keywords

theorem provingcomputer algebraformal methodsprogram verification

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)

Related Items (2)

Formalization of a normalization theorem in simplicial topology ⋮ Modelling algebraic structures and morphisms in ACL2

Uses Software

• Coq
• Kenzo
• QuickCheck

This page was built for publication: Computing in Coq with Infinite Algebraic Data Structures