On behavioural abstraction and behavioural satisfaction in higher-order logic

DOI10.1016/0304-3975(96)00068-0zbMATH Open0874.68196OpenAlexW2073899607MaRDI QIDQ671672FDOQ671672

Authors: Martin Hofmann, Donald Sannella 

Publication date: 27 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(96)00068-0

Recommendations

• On behavioural abstraction and behavioural satisfaction in higher-order logic
• Behavioural and abstractor specifications revisited
• scientific article; zbMATH DE number 1761887
• Behavioural and abstractor specifications

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Cites Work

• On observational equivalence and algebraic specification
• Title not available (Why is that?)
• Completeness in the theory of types
• Title not available (Why is that?)
• Behavioural and abstractor specifications
• Title not available (Why is that?)
• Behavioural theories and the proof of behavioural properties
• The definition of Extended ML: A gentle introduction
• Constructivism in mathematics. An introduction. Volume II
• Toward formal development of programs from algebraic specifications: Implementations revisited
• Title not available (Why is that?)
• Specifications in an arbitrary institution
• Universal algebra in higher types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• Modular correctness proofs of behavioural implementations
• Two impossibility theorems on behaviour specification of abstract data types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Behavioural correctness of data representations

Cited In (16)

• Essential concepts of algebraic specification and program development
• From algebras and coalgebras to dialgebras
• Observational logic, constructor-based logic, and their duality.
• On behavioural abstraction and behavioural satisfaction in higher-order logic
• Behavioural and abstractor specifications revisited
• Behavioural reasoning for conditional equations
• Behavioural theories and the proof of behavioural properties
• Constructor-based observational logic
• Proof systems for structured specifications with observability operators
• Behavioural equivalence and indistinguishability in higher-order typed languages.
• Title not available (Why is that?)
• Closure properties for the class of behavioral models
• The definition of Extended ML: A gentle introduction
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• Behavioural satisfaction and equivalence in concrete model categories
• Observational interpretations of hybrid dynamic logic with binders and silent transitions

This page was built for publication: On behavioural abstraction and behavioural satisfaction in higher-order logic

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