{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:38Z","timestamp":1761611138831},"reference-count":30,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4592,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,1]]},"DOI":"10.1016\/s1571-0661(04)80882-x","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"124-142","source":"Crossref","is-referenced-by-count":11,"special_numbering":"C","title":["Operational Techniques in PVS \u2014 A Preliminary Evaluation"],"prefix":"10.1016","volume":"42","author":[{"given":"Jonathan M.","family":"Ford","sequence":"first","affiliation":[]},{"given":"Ian A.","family":"Mason","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB1","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1090\/S0002-9947-1936-1501858-0","article-title":"Some properties of conversion","volume":"Volume 39","author":"Church","year":"1936","journal-title":"Transactions of the AMS"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB2","unstructured":"J. Crow, S. Owre, J. Rushby, N. Shankar and M. Srivas. A Tutorial Introduction to PVS. Technical report, SRI International, 1995. Presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida."},{"issue":"Number 5","key":"10.1016\/S1571-0661(04)80882-X_NEWBIB3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda-Calculus Notation with Nameless Dummies: a Tool for Automatic Formula Manipulation with Application to the Church-Rosser Theorem","volume":"Volume 34","author":"de Bruijn","year":"1972","journal-title":"Indagationes Mathematicae"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB4","unstructured":"J. Ford. The Church\u2013Rosser theorem in PVS, 2000. PVS dump file (2.4 Megabytes) available at http:\/\/mcs.une.edu.au\/~pvs\/."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB5","unstructured":"J. Ford and I. A. Mason. Establishing a General Context Lemma in PVS. In Proceedings of the 2nd Australasian Workshop on Computational Logic, AWCL'01, 2000. submitted."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB6","unstructured":"R. Harper, H. Honsell and G. Plotkin. A framework for defining logics. In Second Annual Symposium on Logic in Computer Science. IEEE, 1987."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB7","unstructured":"G. Huet. Residual Theory in \u03bb-Calculus: A Formal Development. Technical Report 2009, INRIA, 1993."},{"issue":"Number 3","key":"10.1016\/S1571-0661(04)80882-X_NEWBIB8","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1017\/S0956796800001106","article-title":"Residual Theory in \u03bb-Calculus: A Formal Development","volume":"Volume 4","author":"Huet","year":"1994","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB9","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/363744.363749","article-title":"A correspondence between Algol60 and Church's lambda notation","volume":"Volume 8","author":"Landin","year":"1965","journal-title":"Comm. ACM"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB10","unstructured":"I. A. Mason. Parametric Computation. In James Harland (editor), Proceedings of the Australasian Theory Symposium, CATS '97, pages 103\u2013112, 1997."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB11","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1010052222987","article-title":"Computing with contexts","volume":"Volume 12","author":"Mason","year":"1999","journal-title":"Higher-Order and Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB12","unstructured":"I. A. Mason. A second glance at Feferman-Landin logic, 2000. Invited talk, HOOTS '00 Montreal, Canada, September 2000."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB13","doi-asserted-by":"crossref","unstructured":"I. A. Mason and C. L. Talcott. Programming, transforming, and proving with function abstractions and memories. In Proceedings of the 16th EATCS Colloquium on Automata, Languages, and Programming, Stresa, Volume 372 of Lecture Notes in Computer Science, pages 574\u2013588. Springer-Verlag, 1989.","DOI":"10.1007\/BFb0035784"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB14","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S0956796800000125","article-title":"Equivalence in functional languages with effects","volume":"Volume 1","author":"Mason","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB15","unstructured":"I. A. Mason and C. L. Talcott. Feferman\u2013Landin Logic. In W. Sieg, R. Sommer and C. Talcott (editors), Reflections - A symposium honoring Solomon Feferman on his 70th birthday. to appear in Lecture Notes in Logic, 2000."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB16","series-title":"Typed Lambda Calculi and Applications, Volume 664 of Lecture Notes in Computer Science","first-page":"289","article-title":"Pure Type Systems Formalized","author":"McKinna","year":"1993"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB17","doi-asserted-by":"crossref","DOI":"10.1023\/A:1006294005493","article-title":"Some Lambda Calculus and Type Theory Formalized","volume":"Volume 23","author":"McKinna","year":"1999","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","article-title":"Fully abstract models of typed \u03bb-calculi","volume":"Volume 4","author":"Milner","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB19","series-title":"Automated Deduction \ue4f8 CADE-13, Volume 1104 of Lecture Notes in Computer Science","first-page":"733","article-title":"More Church-Rosser Proofs (in Isabelle\/HOL)","author":"Nipkow","year":"1996"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB20","unstructured":"T. Nipkow. More Church-Rosser Proofs (in Isabelle\/HOL), 2000. to appear in Journal of Automated Reasoning. An abridged version appears as [19]."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB21","doi-asserted-by":"crossref","unstructured":"F. Pfenning. A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework. Technical Report CMU-CS-92-186, Carnegie Mellon University, 1992.","DOI":"10.21236\/ADA256574"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB22","unstructured":"F. Pfenning. A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework. Journal of Automated Reasoning (to appear), 2000. An earlier version appears as [21]."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB23","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value and the lambda calculus","volume":"Volume 1","author":"Plotkin","year":"1975","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB24","unstructured":"R Pollack. Polishing up the Tait-Martin-L\u00f6f Proof of the Church\u2013Rosser Theorem. Unpublished note, available from ftp:\/\/ftp.cs.chalmers.se\/pub\/users\/pollack\/churchrosser.dvi.gz, 1995."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB25","unstructured":"O. Rasmussen. The Church\u2013Rosser theorem in Isabelle: A proof porting experiment. Technical Report 364, University of Cambridge, Computer Laboratory, 1995."},{"issue":"Number 3","key":"10.1016\/S1571-0661(04)80882-X_NEWBIB26","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1145\/44483.44484","article-title":"A Mechanical Proof of the Church-Rosser Theorem","volume":"Volume 35","author":"Shankar","year":"1988","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB27","series-title":"Metamathematics, Machines, and G\u00f6\u00fcdel's Proof","author":"Shankar","year":"1994"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB28","unstructured":"M. Sorensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Technical Report 14, DIKU Report, 1998."},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB29","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1006\/inco.1995.1057","article-title":"Parallel reductions in the \u03bb-calculus","volume":"Volume 118","author":"Takahashi","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80882-X_NEWBIB30","series-title":"Higher Order Operational Techniques in Semantics","article-title":"Reasoning about functions with effects","author":"Talcott","year":"1996"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480882X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480882X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T05:56:16Z","timestamp":1549173376000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610480882X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,1]]},"references-count":30,"alternative-id":["S157106610480882X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80882-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,1]]}}}