Observational equality, now!. Altenkirch, T., McBride, C., & Swierstra, W. In Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07, pages 57, Freiburg, Germany, 2007. ACM Press. ![Observational equality, now! [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper doi abstract bibtex 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].
@inproceedings{altenkirch_observational_2007,
address = {Freiburg, Germany},
title = {Observational equality, now!},
isbn = {978-1-59593-677-6},
url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
doi = {10/dzw23w},
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].},
language = {en},
urldate = {2020-02-14},
booktitle = {Proceedings of the 2007 workshop on {Programming} languages meets program verification - {PLPV} '07},
publisher = {ACM Press},
author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
year = {2007},
pages = {57},
}
Downloads: 0
{"_id":"P9gr7GYgvdz4H6cdH","bibbaseid":"altenkirch-mcbride-swierstra-observationalequalitynow-2007","author_short":["Altenkirch, T.","McBride, C.","Swierstra, W."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Freiburg, Germany","title":"Observational equality, now!","isbn":"978-1-59593-677-6","url":"http://portal.acm.org/citation.cfm?doid=1292597.1292608","doi":"10/dzw23w","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].","language":"en","urldate":"2020-02-14","booktitle":"Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07","publisher":"ACM Press","author":[{"propositions":[],"lastnames":["Altenkirch"],"firstnames":["Thorsten"],"suffixes":[]},{"propositions":[],"lastnames":["McBride"],"firstnames":["Conor"],"suffixes":[]},{"propositions":[],"lastnames":["Swierstra"],"firstnames":["Wouter"],"suffixes":[]}],"year":"2007","pages":"57","bibtex":"@inproceedings{altenkirch_observational_2007,\n\taddress = {Freiburg, Germany},\n\ttitle = {Observational equality, now!},\n\tisbn = {978-1-59593-677-6},\n\turl = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},\n\tdoi = {10/dzw23w},\n\tabstract = {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].},\n\tlanguage = {en},\n\turldate = {2020-02-14},\n\tbooktitle = {Proceedings of the 2007 workshop on {Programming} languages meets program verification - {PLPV} '07},\n\tpublisher = {ACM Press},\n\tauthor = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},\n\tyear = {2007},\n\tpages = {57},\n}\n\n","author_short":["Altenkirch, T.","McBride, C.","Swierstra, W."],"key":"altenkirch_observational_2007-1","id":"altenkirch_observational_2007-1","bibbaseid":"altenkirch-mcbride-swierstra-observationalequalitynow-2007","role":"author","urls":{"Paper":"http://portal.acm.org/citation.cfm?doid=1292597.1292608"},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/SilverSylvester","dataSources":["YCBcQPneB9oxahSnp"],"keywords":[],"search_terms":["observational","equality","now","altenkirch","mcbride","swierstra"],"title":"Observational equality, now!","year":2007}