{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:04:55Z","timestamp":1773097495657,"version":"3.50.1"},"reference-count":14,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5663,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1993,9]]},"abstract":"<jats:p>Type theory allows us to extract from a constructive proof that a specification is satisfiable a program that satisfies the specification. Algorithms for optimization of such programs are currently the object of research.<\/jats:p><jats:p>In this paper we consider one such algorithm, which was described in Beeson (1985) and which we will call \u2018Harrop\u2019. This algorithm greatly simplifies programs extracted from proofs in the Pure Construction Calculus. We use a Partial Equivalence Relation model for higher order lambda calculus, to check that <jats:italic>t<\/jats:italic> and Harrop(<jats:italic>t<\/jats:italic>) return the same outputs from the same inputs, <jats:italic>i.e.<\/jats:italic> that they are <jats:italic>extensionally equal<\/jats:italic>.<\/jats:p><jats:p>As a corollary, we show that it is correct (and, of course, useful) to replace a program <jats:italic>t<\/jats:italic> with Harrop(<jats:italic>t<\/jats:italic>). Such a correctness result has already been proved by M\u00f6hring (M\u00f6hring 1989a, 1989b) using realizability semantics, but we obtain it as a corollary of a new result, the extensional equality between <jats:italic>t<\/jats:italic> and Harrop(<jats:italic>t<\/jats:italic>). Also the semantic method we use is interesting in its own right.<\/jats:p>","DOI":"10.1017\/s0960129500000244","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:02:15Z","timestamp":1236157335000},"page":"309-331","source":"Crossref","is-referenced-by-count":5,"title":["An application of PER models to program extraction"],"prefix":"10.1017","volume":"3","author":[{"given":"Stefano","family":"Berardi","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000244_ref004","volume-title":"Foundation of Constructive Mathematics","author":"Beeson","year":"1980"},{"key":"S0960129500000244_ref003","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1990"},{"key":"S0960129500000244_ref002","volume-title":"Proceedings of the 3rd Italian Conference on Theoretical Computer Science, Mantova 2\u20134 November 1989","author":"Barendregt","year":"1989"},{"key":"S0960129500000244_ref001","volume-title":"The lambda calculus, its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S0960129500000244_ref024","volume":"442","author":"M\u00f6hring","year":"1989","journal-title":"LNCS"},{"key":"S0960129500000244_ref023","volume":"110","author":"M\u00f6hring","year":"1989","journal-title":"Inductive Definitions in the Calculus of Constructions"},{"key":"S0960129500000244_ref005","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundation of Constructive Mathematics, Metamathematical studies","author":"Beeson","year":"1985"},{"key":"S0960129500000244_ref017","first-page":"215","volume":"1","author":"Longo","year":"1990","journal-title":"MSCS"},{"key":"S0960129500000244_ref013","volume-title":"Proceedings of the Second Scandinavian Symposium","author":"Girard","year":"1971"},{"key":"S0960129500000244_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0960129500000244_ref009","volume-title":"Implementing mathematics with Nuprl Proof Development system","author":"Constable","year":"1986"},{"key":"S0960129500000244_ref010","volume":"110","author":"Coquand","year":"1989","journal-title":"Metamathematical investigations of a Calculus of Constructions"},{"key":"S0960129500000244_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"S0960129500000244_ref019","first-page":"73","volume-title":"Logic Colloquium \u201873","author":"Martin-L\u00f6f","year":"1973"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000244","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T21:43:26Z","timestamp":1557956606000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000244\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,9]]},"references-count":14,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,9]]}},"alternative-id":["S0960129500000244"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000244","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,9]]}}}