Certifying properties of an efficient functional program for computing Gröbner bases

DOI10.1016/j.jsc.2007.07.016zbMath1159.13016OpenAlexW2002003982MaRDI QIDQ1012152

J. Santiago Jorge, Jose L. Freire, Victor M. Gulias

Publication date: 14 April 2009

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2007.07.016

zbMATH Keywords

Gröbner basesformal methodsfunctional programmingBuchberger's algorithmsoftware verificationtheorem provers

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10)

Related Items

A generic and executable formalization of signature-based Gröbner basis algorithms, Mathematical Theory Exploration in Theorema: Reduction Rings, A verified common lisp implementation of Buchberger's algorithm in ACL2

Uses Software

• ACL2
• Coq
• FGb
• VoDKA
• PoSSo
• OCaml
• Caml

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Constructing recursion operators in intuitionistic type theory
• The calculus of constructions
• A faster way to count the solutions of inhomogeneous systems of algebraic equations, with applications to cyclic \(n\)-roots
• A new efficient algorithm for computing Gröbner bases \((F_4)\)
• A machine-checked implementation of Buchberger's algorithm
• Artificial Intelligence and Symbolic Computation
• VoDKA: Developing a Video-on-Demand Server using Distributed Functional Programming