<> <http://www.w3.org/2000/01/rdf-schema#comment> "The repository administrator has not yet configured an RDF license."^^<http://www.w3.org/2001/XMLSchema#string> .
<> <http://xmlns.com/foaf/0.1/primaryTopic> <https://discovery.ucl.ac.uk/id/eprint/10030738> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Article> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/terms/title> "Programming and Proving with Distributed Protocols"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/ontology/bibo/abstract> "Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to\r\nimplement correctly. This difficulty arises from two main challenges: (a) correctly implementing\r\ncore system components (e.g., two-phase commit), so all their internal invariants hold, and (b)\r\ncorrectly composing standalone system components into functioning trustworthy applications (e.g.,\r\npersistent storage built on top of a two-phase commit instance). Recent work has developed several\r\napproaches for addressing (a) by means of mechanically verifying implementations of core distributed\r\ncomponents, but no methodology exists to address (b) by composing such verified components into\r\nlarger verified applications. As a result, expensive verification efforts for key system components are\r\nnot easily reusable, which hinders further verification efforts.\r\nIn this paper, we present Disel, the first framework for implementation and compositional\r\nverification of distributed systems and their clients, all within the mechanized, foundational context\r\nof the Coq proof assistant. In Disel, users implement distributed systems using a domain specific\r\nlanguage shallowly embedded in Coq and providing both high-level programming constructs as well\r\nas low-level communication primitives. Components of composite systems are specified in Disel as\r\nprotocols, which capture system-specific logic and disentangle system definitions from implementation\r\ndetails. By virtue of Disel’s dependent type system, well-typed implementations always satisfy\r\ntheir protocols’ invariants and never go wrong, allowing users to verify system implementations\r\ninteractively using Disel’s Hoare-style program logic, which extends state-of-the-art techniques for\r\nconcurrency verification to the distributed setting. By virtue of the substitution principle and frame\r\nrule provided by Disel’s logic, system components can be composed leading to modular, reusable\r\nverified distributed systems.\r\nWe describe Disel, illustrate its use with a series of examples, outline its logic and metatheory,\r\nand report on our experience using it as a framework for implementing, specifying, and verifying\r\ndistributed systems."^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/terms/date> "2018-01-08" .
<https://discovery.ucl.ac.uk/id/document/530335> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Document> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/ontology/bibo/volume> "2" .
<https://discovery.ucl.ac.uk/id/org/ext-2af1883e4bbfa0356fcedb366171cb38> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Organization> .
<https://discovery.ucl.ac.uk/id/org/ext-2af1883e4bbfa0356fcedb366171cb38> <http://xmlns.com/foaf/0.1/name> "ACM"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/terms/publisher> <https://discovery.ucl.ac.uk/id/org/ext-2af1883e4bbfa0356fcedb366171cb38> .
<https://discovery.ucl.ac.uk/id/publication/ext-bc1bad7bc8258b69a65583ac29096cbe> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Collection> .
<https://discovery.ucl.ac.uk/id/publication/ext-bc1bad7bc8258b69a65583ac29096cbe> <http://xmlns.com/foaf/0.1/name> "Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/terms/isPartOf> <https://discovery.ucl.ac.uk/id/publication/ext-bc1bad7bc8258b69a65583ac29096cbe> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/ontology/bibo/status> <http://purl.org/ontology/bibo/status/published> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-3b0779581df20bd784b681276fcb1940> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10030738#authors> .
<https://discovery.ucl.ac.uk/id/eprint/10030738#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_1> <https://discovery.ucl.ac.uk/id/person/ext-3b0779581df20bd784b681276fcb1940> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-6539a0c8fa3211a1fd3281e2f89dc5df> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10030738#authors> .
<https://discovery.ucl.ac.uk/id/eprint/10030738#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_2> <https://discovery.ucl.ac.uk/id/person/ext-6539a0c8fa3211a1fd3281e2f89dc5df> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-611a595373a68a51c7c981d052c658d0> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10030738#authors> .
<https://discovery.ucl.ac.uk/id/eprint/10030738#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_3> <https://discovery.ucl.ac.uk/id/person/ext-611a595373a68a51c7c981d052c658d0> .
<https://discovery.ucl.ac.uk/id/person/ext-3b0779581df20bd784b681276fcb1940> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> .
<https://discovery.ucl.ac.uk/id/person/ext-3b0779581df20bd784b681276fcb1940> <http://xmlns.com/foaf/0.1/givenName> "I"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-3b0779581df20bd784b681276fcb1940> <http://xmlns.com/foaf/0.1/familyName> "Sergey"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-3b0779581df20bd784b681276fcb1940> <http://xmlns.com/foaf/0.1/name> "I Sergey"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-6539a0c8fa3211a1fd3281e2f89dc5df> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> .
<https://discovery.ucl.ac.uk/id/person/ext-6539a0c8fa3211a1fd3281e2f89dc5df> <http://xmlns.com/foaf/0.1/givenName> "JR"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-6539a0c8fa3211a1fd3281e2f89dc5df> <http://xmlns.com/foaf/0.1/familyName> "Wilcox"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-6539a0c8fa3211a1fd3281e2f89dc5df> <http://xmlns.com/foaf/0.1/name> "JR Wilcox"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-611a595373a68a51c7c981d052c658d0> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> .
<https://discovery.ucl.ac.uk/id/person/ext-611a595373a68a51c7c981d052c658d0> <http://xmlns.com/foaf/0.1/givenName> "Z"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-611a595373a68a51c7c981d052c658d0> <http://xmlns.com/foaf/0.1/familyName> "Tatlock"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-611a595373a68a51c7c981d052c658d0> <http://xmlns.com/foaf/0.1/name> "Z Tatlock"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Article> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/ontology/bibo/presentedAt> <https://discovery.ucl.ac.uk/id/event/ext-157752202f9aede7c7202a37c2e8b852> .
<https://discovery.ucl.ac.uk/id/event/ext-157752202f9aede7c7202a37c2e8b852> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Conference> .
<https://discovery.ucl.ac.uk/id/event/ext-157752202f9aede7c7202a37c2e8b852> <http://purl.org/dc/terms/title> "POPL"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/event/ext-157752202f9aede7c7202a37c2e8b852> <http://purl.org/NET/c4dm/event.owl#place> <https://discovery.ucl.ac.uk/id/location/ext-c6967c8c0012410b7a56c636726865f9> .
<https://discovery.ucl.ac.uk/id/event/ext-157752202f9aede7c7202a37c2e8b852> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/NET/c4dm/event.owl#Event> .
<https://discovery.ucl.ac.uk/id/event/ext-157752202f9aede7c7202a37c2e8b852> <http://purl.org/NET/c4dm/event.owl#place> <https://discovery.ucl.ac.uk/id/location/ext-c6967c8c0012410b7a56c636726865f9> .
<https://discovery.ucl.ac.uk/id/location/ext-c6967c8c0012410b7a56c636726865f9> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://www.w3.org/2003/01/geo/wgs84_pos#SpatialThing> .
<https://discovery.ucl.ac.uk/id/location/ext-c6967c8c0012410b7a56c636726865f9> <http://www.w3.org/2000/01/rdf-schema#label> "Los Angeles, CA, USA"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/EPrint> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/ProceedingsSectionEPrint> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/terms/isPartOf> <https://discovery.ucl.ac.uk/id/repository> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530335> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/530335> <http://www.w3.org/2000/01/rdf-schema#label> "Programming and Proving with Distributed Protocols (Text)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://purl.org/dc/elements/1.1/hasVersion> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://eprints.org/ontology/hasAccepted> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530335> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10030738/1/Sergey_disel.pdf> .
<https://discovery.ucl.ac.uk/id/document/530335> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10030738/1/Sergey_disel.pdf> .
<https://discovery.ucl.ac.uk/id/eprint/10030738/1/Sergey_disel.pdf> <http://www.w3.org/2000/01/rdf-schema#label> "Sergey_disel.pdf"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/530336> .
<https://discovery.ucl.ac.uk/id/document/530336> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/530336> <http://www.w3.org/2000/01/rdf-schema#label> "Programming and Proving with Distributed Protocols (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/530336> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530336> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530336> <http://eprints.org/relation/islightboxThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/530337> .
<https://discovery.ucl.ac.uk/id/document/530337> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/530337> <http://www.w3.org/2000/01/rdf-schema#label> "Programming and Proving with Distributed Protocols (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/530337> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530337> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530337> <http://eprints.org/relation/ispreviewThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/530338> .
<https://discovery.ucl.ac.uk/id/document/530338> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/530338> <http://www.w3.org/2000/01/rdf-schema#label> "Programming and Proving with Distributed Protocols (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/530338> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530338> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530338> <http://eprints.org/relation/ismediumThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/530339> .
<https://discovery.ucl.ac.uk/id/document/530339> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/530339> <http://www.w3.org/2000/01/rdf-schema#label> "Programming and Proving with Distributed Protocols (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/530339> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530339> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530339> <http://eprints.org/relation/issmallThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/530340> .
<https://discovery.ucl.ac.uk/id/document/530340> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/530340> <http://www.w3.org/2000/01/rdf-schema#label> "Programming and Proving with Distributed Protocols (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/530340> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530340> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/document/530340> <http://eprints.org/relation/isIndexCodesVersionOf> <https://discovery.ucl.ac.uk/id/document/530335> .
<https://discovery.ucl.ac.uk/id/eprint/10030738> <http://www.w3.org/2000/01/rdf-schema#seeAlso> <https://discovery.ucl.ac.uk/id/eprint/10030738/> .
<https://discovery.ucl.ac.uk/id/eprint/10030738/> <http://purl.org/dc/elements/1.1/title> "HTML Summary of #10030738 \n\nProgramming and Proving with Distributed Protocols\n\n" .
<https://discovery.ucl.ac.uk/id/eprint/10030738/> <http://purl.org/dc/elements/1.1/format> "text/html" .
<https://discovery.ucl.ac.uk/id/eprint/10030738/> <http://xmlns.com/foaf/0.1/primaryTopic> <https://discovery.ucl.ac.uk/id/eprint/10030738> .