Zur Kurzanzeige

Tools for Reasoning about Effectful Declarative Programs

dc.contributor.advisorVoigtländer, Janis
dc.contributor.authorMehner, Stefan Georg
dc.date.accessioned2020-04-21T10:13:35Z
dc.date.available2020-04-21T10:13:35Z
dc.date.issued30.10.2015
dc.identifier.urihttp://hdl.handle.net/20.500.11811/6552
dc.description.abstractIn the pure functional language Haskell, nearly all side-effects that a function can produce have to be noted in its type. This includes input/output, propagation of a state, and nondeterminism. If no side-effects are noted, such a function acts like a mathematical function, i.e., mapping arguments to unique results. In that case, expressions in a program can be reasoned about like mathematical expressions. In addition to this socalled equational reasoning, the type system also enables type based reasoning. One example are free theorems - equations between expressions that are true only due to the types of the expressions involved. Some such statements serve as formal justification for optimization strategies in compilers.
The thesis at hand investigates two generalizations of such methods for programs not free of side-effects, i.e., effectful programs. First, effectful traversals of data structures are being studied. The most important contribution in this part is that a data structure can be lawfully traversed if, and only if, it is isomorphic to a polynomial functor. This result links the widespread interface of traversing to a clear intuition regarding the structure and behavior of the data type. Furthermore, tools are presented facilitating convenient proofs about effectful traversals.
Second, free theorems for the functional-logic language Curry are derived. Due to the close relationship between both languages, Curry can be understood as Haskell with built-in nondeterminism, i.e., a built-in side-effect. Equational and type based reasoning can both be adapted to Curry to a certain degree. In particular, short cut fusion - a very fertile runtime optimization - is enabled for Curry.
dc.language.isoeng
dc.rightsIn Copyright
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/
dc.subject.ddc004 Informatik
dc.titleTools for Reasoning about Effectful Declarative Programs
dc.typeDissertation oder Habilitation
dc.publisher.nameUniversitäts- und Landesbibliothek Bonn
dc.publisher.locationBonn
dc.rights.accessRightsopenAccess
dc.identifier.urnhttps://nbn-resolving.org/urn:nbn:de:hbz:5n-41789
ulbbn.pubtypeErstveröffentlichung
ulbbnediss.affiliation.nameRheinische Friedrich-Wilhelms-Universität Bonn
ulbbnediss.affiliation.locationBonn
ulbbnediss.thesis.levelDissertation
ulbbnediss.dissID4178
ulbbnediss.date.accepted2015-10-16
ulbbnediss.fakultaetMathematisch-Naturwissenschaftliche Fakultät
dc.contributor.coRefereeHanus, Michael


Dateien zu dieser Ressource

Thumbnail

Das Dokument erscheint in:

Zur Kurzanzeige

Die folgenden Nutzungsbestimmungen sind mit dieser Ressource verbunden:

InCopyright