Invariants for the FoCaL language

DOI10.1007/s10472-009-9156-3zbMath1184.68467OpenAlexW1986750872MaRDI QIDQ2379680

Renaud Rioboo

Publication date: 19 March 2010

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-009-9156-3

Mathematics Subject Classification ID

Uses Software

• AXIOM
• Coq
• Isabelle/HOL
• PVS
• MetaPRL
• C-CoRN
• Zenon
• FoCaL
• OpenAxiom

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.
• A constructive algebraic hierarchy in Coq.
• Isabelle/HOL. A proof assistant for higher-order logic
• Algorithms and proofs inheritance in the FOC language
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Setoids in type theory
• How to Write a Proof
• Mathematical Knowledge Management
• Typed Lambda Calculi and Applications

This page was built for publication: Invariants for the FoCaL language