Observational equality, now! Export

@inproceedings{citeulike:3752945, abstract = {This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type which is substitutive , allowing us to reason by replacing equal for equal in propositions; which reflects the observable behaviour of values rather than their construction: in particular, we have extensionality -- functions are equal if they take equal inputs to equal outputs; which retains strong normalisation, decidable typechecking and canonicity --the property that closed normal forms inhabiting datatypes have canonical constructors; which allows inductive data structures to be expressed in terms of a standard characterisation of well-founded trees ; which is presented syntactically --you can implement it directly, and we are doing so this approach stands at the core of Epigram 2; which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system [21]. .}, address = {New York, NY, USA}, author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter}, booktitle = {PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification}, citeulike-article-id = {3752945}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1292597.1292608}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1292597.1292608}, doi = {10.1145/1292597.1292608}, isbn = {978-1-59593-677-6}, keywords = {dependent-types, types}, location = {Freiburg, Germany}, pages = {57--68}, posted-at = {2008-12-07 01:20:39}, priority = {2}, publisher = {ACM}, title = {Observational equality, now!}, url = {http://dx.doi.org/10.1145/1292597.1292608}, year = {2007} }

TY - CONF ID - citeulike:3752945 L3 - citeulike-article-id:3752945 N2 - This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type which is substitutive , allowing us to reason by replacing equal for equal in propositions; which reflects the observable behaviour of values rather than their construction: in particular, we have extensionality -- functions are equal if they take equal inputs to equal outputs; which retains strong normalisation, decidable typechecking and canonicity --the property that closed normal forms inhabiting datatypes have canonical constructors; which allows inductive data structures to be expressed in terms of a standard characterisation of well-founded trees ; which is presented syntactically --you can implement it directly, and we are doing so this approach stands at the core of Epigram 2; which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system [21]. . CY - Freiburg, Germany SN - 978-1-59593-677-6 AD - New York, NY, USA EP - 68 TI - Observational equality, now! PB - ACM T2 - PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification SP - 57 KW - dependent-types KW - types AU - Altenkirch, Thorsten AU - McBride, Conor AU - Swierstra, Wouter PY - 2007/// UR - http://dx.doi.org/10.1145/1292597.1292608 ER -