10 citations · 16 across the 4 of their papers we have counts for
4 papers
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber
Definitions of new symbols merely abbreviate expressions in logical frameworks, and no new facts (regarding previously defined symbols) should hold because of a new definition. In…
Modal Logics for Nominal Transition Systems
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson +2
We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary lo…
The Largest Respectful Function
Joachim Parrow, Tjark Weber
Respectful functions were introduced by Sangiorgi as a compositional tool to formulate short and clear bisimulation proofs. Usually, the larger the respectful function, the easier…
On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code
Hendrik Tews, Marcus Völp, Tjark Weber
In recent projects on operating-system verification, C and C++ data types are often formalized using a semantics that does not fully specify the precise byte encoding of objects. I…