Logical relations (original) (raw)
Logical relations are a proof method employed in programming language semantics to show that two denotational semantics are equivalent. To describe the process, let us denote the two semantics by , where . For each type , there is a particular associated relation between and . This relation is defined such that for each program phrase , the two denotations are related: . Another property of this relation is that related denotations for ground types are equivalent in some sense, usually equal. The conclusion is then that both denotations exhibit equivalent behavior on ground terms, hence are equivalent.
| Property | Value |
|---|---|
| dbo:abstract | Logical relations are a proof method employed in programming language semantics to show that two denotational semantics are equivalent. To describe the process, let us denote the two semantics by , where . For each type , there is a particular associated relation between and . This relation is defined such that for each program phrase , the two denotations are related: . Another property of this relation is that related denotations for ground types are equivalent in some sense, usually equal. The conclusion is then that both denotations exhibit equivalent behavior on ground terms, hence are equivalent. (en) |
| dbo:wikiPageExternalLink | https://poplmark-reloaded.github.io/ https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/ahmed-1.pdf |
| dbo:wikiPageID | 27862709 (xsd:integer) |
| dbo:wikiPageLength | 1170 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1066963179 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Binary_relation dbr:Denotational_semantics dbc:Programming_language_semantics dbr:Data_type dbr:Proof_assistants dbr:Proof_method dbr:Programming_language_semantics |
| dbp:wikiPageUsesTemplate | dbt:Reflist dbt:Formalmethods-stub |
| dcterms:subject | dbc:Programming_language_semantics |
| rdfs:comment | Logical relations are a proof method employed in programming language semantics to show that two denotational semantics are equivalent. To describe the process, let us denote the two semantics by , where . For each type , there is a particular associated relation between and . This relation is defined such that for each program phrase , the two denotations are related: . Another property of this relation is that related denotations for ground types are equivalent in some sense, usually equal. The conclusion is then that both denotations exhibit equivalent behavior on ground terms, hence are equivalent. (en) |
| rdfs:label | Logical relations (en) |
| owl:sameAs | wikidata:Logical relations https://global.dbpedia.org/id/2N2sg |
| prov:wasDerivedFrom | wikipedia-en:Logical_relations?oldid=1066963179&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Logical_relations |
| is dbo:wikiPageRedirects of | dbr:Logical_Relations |
| is dbo:wikiPageWikiLink of | dbr:Denotational_semantics dbr:Logical_Relations dbr:Freyd_cover |
| is foaf:primaryTopic of | wikipedia-en:Logical_relations |