Abstract

This thesis lays the necessary groundwork to automatically and reliably check a certain property of computer programs written in a functional programming language. Because there are many different programming languages, and we do not want to take their specific strategies and features into account, we choose to work on an abstract computation model called conditional term rewriting. The property of conditional term rewriting we are most interested in is confluence, which basically ensures that for a given input a program will always compute the same output, even if it runs concurrently on distributed machines. Within this thesis we first present the basics of conditional term rewriting and related topics and then investigate several known criteria that may be used to show confluence of a given program in the formalism of conditional term rewriting. Additionally we implemented all of the presented methods in an automatic tool which can take a program as input and tries to decide if it is confluent or not. Because this automatic tool may contain bugs, we have also formalized all of the above mentioned criteria in an interactive proof assistant, from which we can automatically generate a certifier that is able to ascertain if our first tool gave the correct answer by checking its output.

BibTeX

@phdthesis{TS17,
  author    = "Thomas Sternagel",
  title     = "Reliable Confluence Analysis of Conditional Term Rewrite Systems",
  school    = "University of Innsbruck",
  year      = 2017
}