HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Algebraic Specifications, Higher-order Types and Set-theoretic Models

Hélène Kirchner 1 Peter D. Mosses
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In most algebraic specification frameworks, the type system is restricted to sorts, subsorts, and first-order function types. This is in marked contrast to the so-called model-oriented frameworks, which provide higher-order types, interpreted set-theoretically as Cartesian products, function spaces, and power-sets. This paper presents a simple framework for algebraic specifications with higher-order types and set-theoretic models. It may be regarded as the basis for a Horn-clause approximation to the Z framework, and has the advantage of being amenable to prototyping and automated reasoning. Standard set-theoretic models are considered, and conditions are given for the existence of initial reducts of such models. Algebraic specifications for various set-theoretic concepts are considered.
Document type :
Journal articles
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:49:10 PM
Last modification on : Friday, February 4, 2022 - 3:34:32 AM


  • HAL Id : inria-00100685, version 1



Hélène Kirchner, Peter D. Mosses. Algebraic Specifications, Higher-order Types and Set-theoretic Models. Journal of Logic and Computation, Oxford University Press (OUP), 2001, 11 (3), pp.453-481. ⟨inria-00100685⟩



Record views