A Calculus Of Higher-order Parameterization For Algebraic Specifications

&
Logic Journal of the IGPL 3 (4):615-641 (1995)
  Copy   BIBTEX

Abstract

A specification language is presented which provides three specification-building operators: amalgamated union, renaming and restriction. The language is enhanced with parameterization over higher-order variables based on the simply typed lambda calculus. Context dependencies that ensure the well-definedness of a parameterized specification, are defined over a calculus of requirements and can be syntactically derived. A contextual proof system for parameterized specifications is also presented, that is correct and relatively complete

Categories

Keywords

Reprint years

DOI

10.1093/jigpal/3.4.615

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,219

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Categorical semantics for higher order polymorphic lambda calculus.R. A. G. Seely - 1987 - Journal of Symbolic Logic 52 (4):969-989.
Higher-order automated theorem proving.Michael Kohlhase - unknown
Formal Mathematics for Verifiably Correct Program Synthesis.Christoph Kreitz - 1996 - Logic Journal of the IGPL 4 (1):75-94.
Definition-like Extensions by Sorts.Claudia Maria & Paulo S. Veloso - 1995 - Logic Journal of the IGPL 3 (4):579-595.
Higher order probabilities and coherence.Soshichi Uchii - 1973 - Philosophy of Science 40 (3):373-381.
On the λY calculus.Rick Statman - 2004 - Annals of Pure and Applied Logic 130 (1-3):325-337.
The Logic of Time Representation.Peter Bernard Ladkin - 1987 - Dissertation, University of California, Berkeley
Third order matching is decidable.Gilles Dowek - 1994 - Annals of Pure and Applied Logic 69 (2-3):135-155.
The modal object calculus and its interpretation.Edward N. Zalta - 1997 - In M. de Rijke (ed.), Advances in Intensional Logic. Kluwer Academic Publishers. pp. 249--279.
The rewriting calculus - part I.H. Cirstea & K. Kirchner - 2001 - Logic Journal of the IGPL 9 (3):339-375.
Normal Forms in Combinatory Logic.Patricia Johann - 1994 - Notre Dame Journal of Formal Logic 35 (4):573-594.
A new formulation of discussive logic.Jerzy Kotas & N. C. A. Costa - 1979 - Studia Logica 38 (4):429 - 445.
Inductive types and type constraints in the second-order lambda calculus.Nax Paul Mendler - 1991 - Annals of Pure and Applied Logic 51 (1-2):159-172.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
CERES in higher-order logic.Stefan Hetzl, Alexander Leitsch & Daniel Weller - 2011 - Annals of Pure and Applied Logic 162 (12):1001-1034.

Analytics

Added to PP
2015-02-04

Downloads
4 (#1,556,099)

6 months
2 (#1,157,335)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references