Fast and loose reasoning is morally correct Export

@inproceedings{citeulike:558255, abstract = {Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values.It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation.}, address = {New York, NY, USA}, author = {Danielsson, Nils A. and Hughes, John and Jansson, Patrik and Gibbons, Jeremy}, booktitle = {POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, citeulike-article-id = {558255}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1111037.1111056}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1111037.1111056}, doi = {10.1145/1111037.1111056}, isbn = {1-59593-027-2}, keywords = {call-by-name, call-by-value, category-theory, denotational-semantics, functional-programming, haskell, laziness, lazy-evaluation, logical-relations, ml, selective-strictness, seq, strict-evaluation, types}, location = {Charleston, South Carolina, USA}, month = {January}, number = {1}, pages = {206--217}, posted-at = {2006-03-21 11:28:11}, priority = {0}, publisher = {ACM}, title = {Fast and loose reasoning is morally correct}, url = {http://dx.doi.org/10.1145/1111037.1111056}, volume = {41}, year = {2006} }

TY - CONF ID - citeulike:558255 L3 - citeulike-article-id:558255 N2 - Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values.It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation. CY - Charleston, South Carolina, USA IS - 1 SN - 1-59593-027-2 AD - New York, NY, USA EP - 217 TI - Fast and loose reasoning is morally correct PB - ACM VL - 41 T2 - POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages SP - 206 KW - call-by-name KW - call-by-value KW - category-theory KW - denotational-semantics KW - functional-programming KW - haskell KW - laziness KW - lazy-evaluation KW - logical-relations KW - ml KW - selective-strictness KW - seq KW - strict-evaluation KW - types AU - Danielsson, Nils AU - Hughes, John AU - Jansson, Patrik AU - Gibbons, Jeremy PY - 2006/01// UR - http://dx.doi.org/10.1145/1111037.1111056 ER -