Object oriented institutions to specify symbolic computation systems

DOI10.1051/ITA:2007015MaRDI QIDQ5441547zbMATH OpenOpenAlexFDO

Authors César Domínguez, Laureano Lambán, Julio Rubio

Publication date 15 February 2008

Published in RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL http://www.numdam.org/item?id=ITA_2007__41_2_191_0, https://semanticscholar.org/paper/7c46b7e42e725ba051f0c4b7254824bbd559860a

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 2000439
• scientific article; zbMATH DE number 6118174
• An object-oriented interpretation of the EAT system
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• scientific article; zbMATH DE number 1368950

Cites work

• A coalgebraic equational approach to specifying observational structures
• A hidden agenda
• A hidden Herbrand theorem: Combining the object and logic paradigms
• An object-oriented interpretation of the EAT system
• Constructive algebraic topology
• Constructor-based observational logic
• Diagrammatic specifications
• scientific article; zbMATH DE number 1189281 (Why is no real title available?)
• scientific article; zbMATH DE number 1189282 (Why is no real title available?)
• scientific article; zbMATH DE number 46995 (Why is no real title available?)
• scientific article; zbMATH DE number 1350001 (Why is no real title available?)
• scientific article; zbMATH DE number 2000439 (Why is no real title available?)
• scientific article; zbMATH DE number 1487499 (Why is no real title available?)
• scientific article; zbMATH DE number 1418819 (Why is no real title available?)
• Institution morphisms
• Institutions: abstract model theory for specification and programming
• Modeling inheritance as coercion in a symbolic computation system
• Observational logic, constructor-based logic, and their duality.
• On institutions for modular coalgebraic specifications.
• Specification of abstract data types
• Towards heterogeneous specifications
• Universal coalgebra: A theory of systems

Cited in

(13)

• An object-oriented interpretation of the EAT system
• Formalization of a normalization theorem in simplicial topology
• scientific article; zbMATH DE number 1617302 (Why is no real title available?)
• A parameterization process: from a functorial point of view
• Diagrammatic logic applied to a parameterisation process
• ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
• scientific article; zbMATH DE number 2000439 (Why is no real title available?)
• scientific article; zbMATH DE number 5199000 (Why is no real title available?)
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Mediated Access to Symbolic Computation Systems
• A case-study in algebraic manipulation using mechanized reasoning tools
• Effective homology of bicomplexes, formalized in Coq
• Generating certified code from formal proofs: a case study in homological algebra

Describes a project that uses

Uses Software

• Kenzo
• EAT

This page was built for publication: Object oriented institutions to specify symbolic computation systems

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