Tue 17 Jan 2023 11:00 - 11:30 at Scollay - 3 talks Chair(s): Casper Bach Poulsen

Semantics-preserving source-to-source program transformations, such as optimization and refactoring, are essential for software development. Such transformations are often defined by rewriting rules describing which part of a program must be replaced with which subprogram. The main obstacle to designing a transformation is to prove its semantics preservation. Rewriting-rule-based frameworks alleviate this difficulty by giving proof guidelines or automating the proofs. Unfortunately, each framework is applicable to a restricted set of transformations due to a fixed definition of semantics preservation. Cousot and Cousot’s semantic transformation framework resolves this problem by leaving a space for its users to define a proper semantics preservation property. However, the framework does not exploit the characteristic of rewriting rules and fails to ease the proofs. In this work, we define a semantic transformation framework tailored to rewriting rules by refining Cousot and Cousot’s framework. Our framework facilitates modular proofs by providing syntax-directed guidelines and theorems that simplify proofs. We show the versatility of our framework by proving the semantics preservation of six well-known transformations.

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

11:00 - 12:30
3 talksPEPM at Scollay
Chair(s): Casper Bach Poulsen Delft University of Technology
11:00
30m
Talk
Semantic Transformation Framework for Rewriting Rules
PEPM
Jihee Park KAIST, Jaemin Hong KAIST, Sukyoung Ryu KAIST
11:30
30m
Talk
Symbolic Execution of Hadamard-Toffoli Quantum Circuits
PEPM
Jacques Carette McMaster University, Gerardo Ortiz Indiana University, Amr Sabry Indiana University
12:00
30m
Talk
Generating Programs for Polynomial Multiplication with Correctness Assurance
PEPM
Ryo Tokuda University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba