In *Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07*, pages 57, Freiburg, Germany, 2007. ACM Press.

Paper doi abstract bibtex

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 reﬂects 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 reﬂects 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