{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/112004"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/112004","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Making discrete decisions based on continuous values","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Sherman, Benjamin (Benjamin Marc)"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.","school":null,"contributors":[],"advisors":["Adam Chlipala and Michael Carbin."],"committee_chairs":[],"committee_members":[],"year":2017,"date_issued":"2017","date_published":"2017","updated_at":"2026-07-22T22:22:22Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"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."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/112004","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Adam Chlipala and Michael Carbin."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Sherman, Benjamin (Benjamin Marc)"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2017-10-30T15:03:58Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2017-10-30T15:03:58Z"]},{"key":"dc:date.issued","label":"Date","values":["2017"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["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."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/112004"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis: S.M., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017.","This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 99-102)."]},{"key":"dc:description.abstract","label":"Abstract","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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["S.M."]},{"key":"dc:title","label":"Title","values":["Making discrete decisions based on continuous values"]}]}],"canonical_facts":{"dc:contributor.advisor":["Adam Chlipala and Michael Carbin."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Sherman, Benjamin (Benjamin Marc)"],"dc:date.accessioned":["2017-10-30T15:03:58Z"],"dc:date.available":["2017-10-30T15:03:58Z"],"dc:date.issued":["2017"],"dc:description":["Thesis: S.M., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017.","This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 99-102)."],"dc:description.abstract":["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."],"dc:description.degree":["S.M."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/112004"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"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."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Making discrete decisions based on continuous values"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:22:22Z"}