On behavioural abstraction and behavioural satisfaction in higher-order logic

DOI10.1016/0304-3975(96)00068-0zbMath0874.68196OpenAlexW2073899607MaRDI QIDQ671672

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

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

Related Items

Observational logic, constructor-based logic, and their duality. ⋮ Constructor-based observational logic ⋮ Closure properties for the class of behavioral models ⋮ Essential concepts of algebraic specification and program development ⋮ Proof systems for structured specifications with observability operators ⋮ The definition of Extended ML: A gentle introduction ⋮ Observational interpretations of hybrid dynamic logic with binders and silent transitions ⋮ Behavioural theories and the proof of behavioural properties ⋮ From Algebras and Coalgebras to Dialgebras ⋮ Behavioural reasoning for conditional equations ⋮ Behavioural and abstractor specifications revisited ⋮ On behavioural abstraction and behavioural satisfaction in higher-order logic

Cites Work

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