Making discrete decisions based on continuous values

Many safety-critical software systems are cyber-physical systems that compute with continuous values; confirming their safety requires guaranteeing the accuracy of their computations. It is impossible for these systems to compute (total and deterministic) discrete computations (e.g., decisions) based on connected input spaces such as R. We propose a programming language based on constructive topology, whose types are spaces and programs are executable continuous maps, that facilitates making formal guarantees of accuracy of computed results. We demonstrate that discrete decisions can be made based on continuous values by permitting nondeterminism. This thesis describes variants of the programming language allowing nondeterminism and/or partiality, and introduces two tools for creating nondeterministic programs on spaces. Overlapping pattern matching is a generalization of pattern matching in functional programming, where patterns need not represent decidable predicates and also may overlap, allowing potentially nondeterministic behavior in overlapping regions. Binary covers, which are pairs of predicates such that at least one of them holds, yield a formal logic for constructing approximate decision procedures.

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2017

Author dc:creator

• Sherman, Benjamin (Benjamin Marc)

Advisor dc:contributor.advisor

• Adam Chlipala and Michael Carbin.

• Electrical Engineering and Computer Science.

Statement dc:rights

• MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/112004

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/112004