Order-sorted parameterization and induction

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Parameterization is one of the most powerful features to make specifications and declarative programs modular and reusable, and our best hope for scaling up formal verification efforts. This paper studies order-sorted parameterization at three different levels: (i) its mathematical semantics; (ii) its operational semantics by term rewriting; and (iii) the inductive reasoning principles that can soundly be used to prove properties about such specifications. It shows that achieving the desired properties at each of these three levels is a considerably subtler matter than for many-sorted specifications, but that such properties can be attained under reasonable conditions.

Original languageEnglish (US)
Title of host publicationSemantics and Algebraic Specification - Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday
EditorsJens Palsberg
Pages43-80
Number of pages38
DOIs
StatePublished - Nov 2 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5700 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Order-sorted parameterization and induction'. Together they form a unique fingerprint.

Cite this