Invariants for the FoCaL language

DOI10.1007/S10472-009-9156-3zbMATH Open1184.68467OpenAlexW1986750872MaRDI QIDQ2379680FDOQ2379680

Authors: 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

Recommendations

• Algorithms and proofs inheritance in the FOC language
• Mathematical knowledge management in Foc
• scientific article; zbMATH DE number 1497749
• Typed Lambda Calculi and Applications
• A Coq formalization of finitely presented modules

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99) Abstract data types; algebraic specification (68Q65) Algebraic structures (08A99)

Cites Work

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

Cited In (1)

• Mathematical knowledge management in Foc

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2379680)