Master's Thesis

Semantics of an Intermediate Language for Program Transformation
Advisors: Prof. Sebastian Hack, Prof. Gert Smolka
Submission date: May 28th 2013
Download Coq development Thesis

Abstract

We present an idealized intermediate language designed to investigate the translation between a functional intermediate representation and an imperative register transfer language as it occurs in the back-end of a compiler. A key feature of our language is its dual semantics: there is a functional and an imperative interpretation. The functional interpretation is equipped with a fully compositional notion of program equivalence that is useful for the integration of advanced optimizations. The imperative interpretation is close to assembly and can serve as a faithful model of a low-level (virtual) machine.

Programs on which both interpretations coincide are identified via a novel condition we call coherence. Translating between the two interpretations reduces to establishing coherence. Establishing coherence under preservation of the imperative semantics can be seen as a form of SSA construction. To establish coherence under preservation of the functional semantics it suffices to α-rename. An α-renaming that establishes coherence can be understood as a register assignment. From coherence, decidable correctness conditions for the translations between the two interpretations are derived.

The language together with its theory is implemented using the Coq proof assistant without axioms. Translations between the two interpretations are implemented as extractable, translation-validated transformations realizing SSA construction and register assignment.

Proposal Talk

Abstract

Program representations in static single assignment (SSA) form have become standard in compiler construction, because the SSA condition eases the specification and implementation of program transformations.

We present a functional intermediate language that is well suited to represent programs in SSA form, and discuss requirements for a compositional notion of program equivalence. We outline what needs to be done to integrate the language into a simple compilation process and discuss challenges and directions of my master's thesis.

The work is done using the Coq proof assistant.

Slides

The slides can be downloaded here.

 

Bachelor's Thesis

Terminating Tableaux for Modal Logic with Transitive Closure
Advisors: Mark Kaminski, Gert Smolka
Responsible Professor: Gert Smolka

Abstract

We present a terminating tableau system for the modal logic K*. K* extends the basic modal logic K with a reflexive transitive closure operator for relations and is a proper fragment of propositional dynamic logic.

We investigate two different approaches to achieve termination, namely chain-based blocking and pattern-based blocking. Pattern based-blocking has not been applied to a modal logic with a reflexive transitive closure operator.

We have a modular completeness proof that adapts to both termination approaches. Extending completeness arguments for a related description logic, we establish a strength- ened soundness property of our calculus that we call straightness. Using this property we are able to prove both verification and refutation soundness.

Downloads

The thesis can be downloaded here.

Introduction Talk

Abstract

Propositional dynamic logic is a modal logic with extended relational expressivity. It allows formulation of program invariants, such as properties of simple while loops.

In this talk, we present a well-known decidability result for PDL. The result is obtained by showing that PDL has the small model property. The proof employs a filtration argument. Filtration is a technique from modal logic that generates finite models by identifying equivalent states.

Slides

The slides can be downloaded here.

Proposal Talk

Abstract

In my first talk I have presented a decidability result for PDL. Now I am interested in a tableau-based decision procedure for a fragment of PDL where relational expressivity has been stripped to only allow the Kleene star.

I'll show what I've learned about tableau derivations, give my intuitions, and present open problems with transferring the ideas to PDL. In the end, I will give an overview about what I want to accomplish in my bachelor's thesis.

Slides

The slides can be downloaded here.

Final Talk

The final talk presents material from the first chapters of the thesis.

Slides

The slides can be downloaded here .