On behavioural abstraction and behavioural satisfaction in higher-order logic

DOI10.1016/0304-3975(96)00068-0MaRDI QIDQ671672zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 3819086 (Why is no real title available?)
• scientific article; zbMATH DE number 3911679 (Why is no real title available?)
• scientific article; zbMATH DE number 4088907 (Why is no real title available?)
• scientific article; zbMATH DE number 3776831 (Why is no real title available?)
• scientific article; zbMATH DE number 3529404 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 1142318 (Why is no real title available?)
• scientific article; zbMATH DE number 1368954 (Why is no real title available?)
• scientific article; zbMATH DE number 3999267 (Why is no real title available?)
• scientific article; zbMATH DE number 4113952 (Why is no real title available?)
• scientific article; zbMATH DE number 785047 (Why is no real title available?)
• scientific article; zbMATH DE number 1418817 (Why is no real title available?)
• Behavioural and abstractor specifications
• Behavioural correctness of data representations
• Behavioural theories and the proof of behavioural properties
• Completeness in the theory of types
• Constructivism in mathematics. An introduction. Volume II
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• Modular correctness proofs of behavioural implementations
• On observational equivalence and algebraic specification
• Specifications in an arbitrary institution
• The definition of Extended ML: A gentle introduction
• Toward formal development of programs from algebraic specifications: Implementations revisited
• Two impossibility theorems on behaviour specification of abstract data types
• Universal algebra in higher types

Cited in

(16)

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

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)