<> <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/10115802> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/AcademicArticle> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Article> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/terms/title> "Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/ontology/bibo/abstract> "We study a syntax for specifying quantitative “assertions” - functions mapping program states to numbers - for probabilistic program verification. We prove that our syntax is expressive in the following sense: Given any probabilistic program C, if a function f is expressible in our syntax, then the function mapping each initial state σ to the expected value of f evaluated in the final states reached after termination C on σ (also called the weakest preexpectation wp[C](f)) is also expressible in our syntax. As a consequence, we obtain a relatively complete verification system for verifying expected values and probabilities in the sense of Cook: Apart from a single reasoning step about the inequality of two functions given as syntactic expressions in our language, given f, g, and C, we can check whether g ≤ wp[C](f)."^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/terms/date> "2021-01" .
<https://discovery.ucl.ac.uk/id/document/1304178> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Document> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/ontology/bibo/volume> "5" .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/ontology/bibo/issue> "POPL" .
<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/10115802> <http://purl.org/dc/terms/publisher> <https://discovery.ucl.ac.uk/id/org/ext-2af1883e4bbfa0356fcedb366171cb38> .
<https://discovery.ucl.ac.uk/id/publication/ext-e7859950da9b9dc1e9414b754269e371> <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-e7859950da9b9dc1e9414b754269e371> <http://xmlns.com/foaf/0.1/name> "Proceedings of the ACM on Programming Languages"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/terms/isPartOf> <https://discovery.ucl.ac.uk/id/publication/ext-e7859950da9b9dc1e9414b754269e371> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/ontology/bibo/status> <http://purl.org/ontology/bibo/status/published> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-403163b2ae78a0fa6ecbcc70b0f9c51c> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10115802#authors> .
<https://discovery.ucl.ac.uk/id/eprint/10115802#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_1> <https://discovery.ucl.ac.uk/id/person/ext-403163b2ae78a0fa6ecbcc70b0f9c51c> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-a37bd7607b0058eb2c5ec47db97a59da> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10115802#authors> .
<https://discovery.ucl.ac.uk/id/eprint/10115802#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_2> <https://discovery.ucl.ac.uk/id/person/ext-a37bd7607b0058eb2c5ec47db97a59da> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-b2a6e38f7525fec1c2142c24818e388d> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10115802#authors> .
<https://discovery.ucl.ac.uk/id/eprint/10115802#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_3> <https://discovery.ucl.ac.uk/id/person/ext-b2a6e38f7525fec1c2142c24818e388d> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-83a6ea369650496a3bfd57e836ab447d> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10115802#authors> .
<https://discovery.ucl.ac.uk/id/eprint/10115802#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_4> <https://discovery.ucl.ac.uk/id/person/ext-83a6ea369650496a3bfd57e836ab447d> .
<https://discovery.ucl.ac.uk/id/person/ext-b2a6e38f7525fec1c2142c24818e388d> <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-b2a6e38f7525fec1c2142c24818e388d> <http://xmlns.com/foaf/0.1/givenName> "J-P"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-b2a6e38f7525fec1c2142c24818e388d> <http://xmlns.com/foaf/0.1/familyName> "Katoen"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-b2a6e38f7525fec1c2142c24818e388d> <http://xmlns.com/foaf/0.1/name> "J-P Katoen"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-403163b2ae78a0fa6ecbcc70b0f9c51c> <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-403163b2ae78a0fa6ecbcc70b0f9c51c> <http://xmlns.com/foaf/0.1/givenName> "K"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-403163b2ae78a0fa6ecbcc70b0f9c51c> <http://xmlns.com/foaf/0.1/familyName> "Batz"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-403163b2ae78a0fa6ecbcc70b0f9c51c> <http://xmlns.com/foaf/0.1/name> "K Batz"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-83a6ea369650496a3bfd57e836ab447d> <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-83a6ea369650496a3bfd57e836ab447d> <http://xmlns.com/foaf/0.1/givenName> "C"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-83a6ea369650496a3bfd57e836ab447d> <http://xmlns.com/foaf/0.1/familyName> "Matheja"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-83a6ea369650496a3bfd57e836ab447d> <http://xmlns.com/foaf/0.1/name> "C Matheja"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-a37bd7607b0058eb2c5ec47db97a59da> <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-a37bd7607b0058eb2c5ec47db97a59da> <http://xmlns.com/foaf/0.1/givenName> "BL"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-a37bd7607b0058eb2c5ec47db97a59da> <http://xmlns.com/foaf/0.1/familyName> "Kaminski"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-a37bd7607b0058eb2c5ec47db97a59da> <http://xmlns.com/foaf/0.1/name> "BL Kaminski"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/EPrint> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/ArticleEPrint> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/terms/isPartOf> <https://discovery.ucl.ac.uk/id/repository> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304178> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/1304178> <http://www.w3.org/2000/01/rdf-schema#label> "Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning (Text)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://purl.org/dc/elements/1.1/hasVersion> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://eprints.org/ontology/hasPublished> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304178> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10115802/1/Kaminski_3434320.pdf> .
<https://discovery.ucl.ac.uk/id/document/1304178> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10115802/1/Kaminski_3434320.pdf> .
<https://discovery.ucl.ac.uk/id/eprint/10115802/1/Kaminski_3434320.pdf> <http://www.w3.org/2000/01/rdf-schema#label> "Kaminski_3434320.pdf"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1304180> .
<https://discovery.ucl.ac.uk/id/document/1304180> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/1304180> <http://www.w3.org/2000/01/rdf-schema#label> "Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/1304180> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304180> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304180> <http://eprints.org/relation/ispreviewThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304180> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10115802/3/preview.jpg> .
<https://discovery.ucl.ac.uk/id/document/1304180> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10115802/3/preview.jpg> .
<https://discovery.ucl.ac.uk/id/eprint/10115802/3/preview.jpg> <http://www.w3.org/2000/01/rdf-schema#label> "preview.jpg"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1304181> .
<https://discovery.ucl.ac.uk/id/document/1304181> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/1304181> <http://www.w3.org/2000/01/rdf-schema#label> "Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/1304181> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304181> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304181> <http://eprints.org/relation/ismediumThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304181> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10115802/4/medium.jpg> .
<https://discovery.ucl.ac.uk/id/document/1304181> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10115802/4/medium.jpg> .
<https://discovery.ucl.ac.uk/id/eprint/10115802/4/medium.jpg> <http://www.w3.org/2000/01/rdf-schema#label> "medium.jpg"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1304182> .
<https://discovery.ucl.ac.uk/id/document/1304182> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/1304182> <http://www.w3.org/2000/01/rdf-schema#label> "Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/1304182> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304182> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304182> <http://eprints.org/relation/issmallThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304182> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10115802/5/small.jpg> .
<https://discovery.ucl.ac.uk/id/document/1304182> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10115802/5/small.jpg> .
<https://discovery.ucl.ac.uk/id/eprint/10115802/5/small.jpg> <http://www.w3.org/2000/01/rdf-schema#label> "small.jpg"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1304183> .
<https://discovery.ucl.ac.uk/id/document/1304183> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/1304183> <http://www.w3.org/2000/01/rdf-schema#label> "Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/1304183> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304183> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304183> <http://eprints.org/relation/islightboxThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304183> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10115802/6/lightbox.jpg> .
<https://discovery.ucl.ac.uk/id/document/1304183> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10115802/6/lightbox.jpg> .
<https://discovery.ucl.ac.uk/id/eprint/10115802/6/lightbox.jpg> <http://www.w3.org/2000/01/rdf-schema#label> "lightbox.jpg"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1304184> .
<https://discovery.ucl.ac.uk/id/document/1304184> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/1304184> <http://www.w3.org/2000/01/rdf-schema#label> "Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/1304184> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304184> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304184> <http://eprints.org/relation/isIndexCodesVersionOf> <https://discovery.ucl.ac.uk/id/document/1304178> .
<https://discovery.ucl.ac.uk/id/document/1304184> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10115802/7/indexcodes.txt> .
<https://discovery.ucl.ac.uk/id/document/1304184> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10115802/7/indexcodes.txt> .
<https://discovery.ucl.ac.uk/id/eprint/10115802/7/indexcodes.txt> <http://www.w3.org/2000/01/rdf-schema#label> "indexcodes.txt"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/10115802> <http://www.w3.org/2000/01/rdf-schema#seeAlso> <https://discovery.ucl.ac.uk/id/eprint/10115802/> .
<https://discovery.ucl.ac.uk/id/eprint/10115802/> <http://purl.org/dc/elements/1.1/title> "HTML Summary of #10115802 \n\nRelatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning\n\n" .
<https://discovery.ucl.ac.uk/id/eprint/10115802/> <http://purl.org/dc/elements/1.1/format> "text/html" .
<https://discovery.ucl.ac.uk/id/eprint/10115802/> <http://xmlns.com/foaf/0.1/primaryTopic> <https://discovery.ucl.ac.uk/id/eprint/10115802> .