NDLI: Institutions: abstract model theory for specification and programming

Content Provider	ACM Digital Library
Author	Goguen, Joseph A. Burstall, Rod M.
Copyright Year	1992
Abstract	There is a population explosion among the logical systems used in computing science. Examples include first-order logic, equational logic, Horn-clause logic, higher-order logic, infinitary logic, dynamic logic, intuitionistic logic, order-sorted logic, and temporal logic; moreover, there is a tendency for each theorem prover to have its own idiosyncratic logical system. The concept of $\textit{institution}$ is introduced to formalize the informal notion of “logical system.” The major requirement is that there is a satisfaction relation between models and sentences that is consistent under change of notation. Institutions enable abstracting away from syntactic and semantic detail when working on language structure “in-the-large”; for example, we can define language features for building large logical system. This applies to both specification languages and programming languages. Institutions also have applications to such areas as database theory and the semantics of artificial and natural languages. A first main result of this paper says that any institution such that signatures (which define notation) can be glued together, also allows gluing together theories (which are just collections of sentences over a fixed signature). A second main result considers when theory structuring is preserved by institution morphisms. A third main result gives conditions under which it is sound to use a theorem prover for one institution on theories from another. A fourth main result shows how to extend institutions so that their theories may include, in addition to the original sentences, various kinds of constraint that are useful for defining abstract data types, including both “data” and “hierarchy” constraints. Further results show how to define institutions that allow sentences and constraints from two or more institutions. All our general results apply to such “duplex” and “multiplex” institutions.
Starting Page	95
Ending Page	146
Page Count	52
File Format	PDF
ISSN	00045411
e-ISSN	1557735X
DOI	10.1145/147508.147524
Journal	Journal of the ACM (JACM)
Volume Number	39
Issue Number	1
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1992-01-02
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Information Systems Control and Systems Engineering Artificial Intelligence Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A Formal Method for the Abstract Specification of Software

On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types

Programming Language for Automata

Micro-Programming

Backtrack Programming

Contributions to the Theory of Logic Programming

Computer Programming for Young Students

An Abstract Machine for Symbolic Computation

Toward Abstract Numerical Analysis

Institutions: abstract model theory for specification and programming

Similar Documents

A Formal Method for the Abstract Specification of Software

On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types

Programming Language for Automata

Micro-Programming

Backtrack Programming

Contributions to the Theory of Logic Programming

Computer Programming for Young Students

An Abstract Machine for Symbolic Computation

Toward Abstract Numerical Analysis

Institutions: abstract model theory for specification and programming