Check out my first novel, midnight's simulacra!
Programming Language Theory: Difference between revisions
From dankwiki
| Line 143: | Line 143: | ||
* ''Denotational'' semantics map between different ''semantic domains'' (the investigation of which constitutes [http://en.wikipedia.org/wiki/Domain_theory domain theory]) using ''interpretation functions''. Domains are interesting if results have been proven for their properties, such as termination and safety results. Denotational semantics can thus lead to proof schemas for a language, but meaningful interpretation functions seem to largely require domain-driven language design. | * ''Denotational'' semantics map between different ''semantic domains'' (the investigation of which constitutes [http://en.wikipedia.org/wiki/Domain_theory domain theory]) using ''interpretation functions''. Domains are interesting if results have been proven for their properties, such as termination and safety results. Denotational semantics can thus lead to proof schemas for a language, but meaningful interpretation functions seem to largely require domain-driven language design. | ||
* While operational and denotational semantics define the behaviors of programs, and then prove laws about them, ''axiomatic'' semantics define the behavior of the language in terms of these laws themselves. As Pierce says: "The meaning of a term is just what can be proved about it." | * While operational and denotational semantics define the behaviors of programs, and then prove laws about them, ''axiomatic'' semantics define the behavior of the language in terms of these laws themselves. As Pierce says: "The meaning of a term is just what can be proved about it." | ||
* Van Roy and Hiridi also mention ''logical'' semantics, which define a statement as a model of logical theory. This is claimed to work well for declarative and logical programming models. | |||
==Sources== | ==Sources== | ||
