Computer science/Semantics and reasoning

Subject Classification

ACM: Theory of computation~Semantics and reasoning

AMS: Computer science / Theory of computing / Semantics in the theory of computing

2025

The Weak Spectroscopy Game to Characterize Behavioral Equivalences

by Lisa A. Barthel, Leonard M. Hübner, Caroline Lemke, Karl P. P. Mattes, Lenard Mollenkopf and Benjamin Bisping

Nov 17

Z Mathematical Toolkit in Isabelle/HOL

by Simon Foster, Pedro Ribeiro, Frank Zeyda and Jim Woodcock

Oct 16

Shallow Expressions

by Simon Foster

May 16

Ultrametric Structure for Restriction Spaces

by Benoît Ballenghien, Benjamin Puyobro and Burkhart Wolff

May 07

Restriction Spaces: a Fixed-Point Theory

by Benoît Ballenghien, Benjamin Puyobro and Burkhart Wolff

May 07

CSP Semantics over Restriction Spaces

by Benoît Ballenghien and Burkhart Wolff

May 07

Differential Privacy

by Tetsuya Sato and Yasuhiko Minamide

Jan 07

Differential Privacy using Quasi-Borel Spaces

by Michikazu Hirata

Jan 07

2024

NREST: Nondeterministc RESult monad with Time

by Maximilian P. L. Haslbeck

Sep 16

Extension of Stateful Intransitive Noninterference with Inputs, Outputs, and Nondeterminism in Language IMP

by Pasquale Noce

Sep 02

A formalized programming language with speculative execution

by Jamie Wright and Andrei Popescu

Aug 16

Definitive Set Semantics for LTL3

by Rayhana Amjad, Rob van Glabbeek and Liam O'Connor

Aug 12

Isabelle/DOF

by Achim D. Brucker, Nicolas Méric and Burkhart Wolff

Apr 26

AutoCorres2

by Matthew Brecknell, David Greenaway, Johannes Hölzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch and Simon Wimmer

Apr 17

2023

Operational Semantics formally proven in HOL-CSP

by Benoît Ballenghien and Burkhart Wolff

Dec 24

HOL-CSPM - Architectural operators for HOL-CSP

by Benoît Ballenghien, Safouan Taha and Burkhart Wolff

Dec 05

Transport via Partial Galois Connections and Equivalences

by Kevin Kappelmann

Oct 11

S-Finite Measure Monad on Quasi-Borel Spaces

by Michikazu Hirata and Yasuhiko Minamide

Aug 08

Modal quantales, involutive quantales, Dedekind Quantales

by Georg Struth and Cameron Calk

Jul 25

2022

A Formal CHERI-C Memory Model

by Seung Hoon Park

Nov 25

Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL

by Diego Marmsoler and Achim D. Brucker

Jul 18

Quasi-Borel Spaces

by Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato

Feb 03

2021

Quantum and Classical Registers

by Dominique Unruh

Oct 28

X86 instruction semantics and basic block symbolic execution

by Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag and Binoy Ravindran

Oct 13

2020

The HOL-CSP Refinement Toolkit

by Safouan Taha, Burkhart Wolff and Lina Ye

Nov 19

2019

Isabelle/C

by Frédéric Tuong and Burkhart Wolff

Oct 22

Clean - An Abstract Imperative Programming Language and its Theory

by Frédéric Tuong and Burkhart Wolff

Oct 04

A Formal Development of a Polychronous Polytimed Coordination Language

by Hai Nguyen Van, Frédéric Boulanger and Burkhart Wolff

Jul 30

HOL-CSP Version 2.0

by Benoît Ballenghien, Safouan Taha, Burkhart Wolff and Lina Ye

Apr 26

Quantum Hoare Logic

by Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying and Naijun Zhan

Mar 24

2018

Transformer Semantics

by Georg Struth

Dec 11

2016

The Imperative Refinement Framework

by Peter Lammich

Aug 08

2013

The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

by Joachim Breitner

Jan 31

2012

Refinement for Monadic Programs

by Peter Lammich

Jan 30