{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,11]],"date-time":"2024-04-11T08:25:19Z","timestamp":1712823919230},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1992,12,1]],"date-time":"1992-12-01T00:00:00Z","timestamp":723168000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1992,12]]},"DOI":"10.1007\/bf00245294","type":"journal-article","created":{"date-parts":[[2004,11,7]],"date-time":"2004-11-07T23:31:19Z","timestamp":1099870279000},"page":"309-354","source":"Crossref","is-referenced-by-count":54,"title":["Using typed lambda calculus to implement formal systems on a machine"],"prefix":"10.1007","volume":"9","author":[{"given":"Arnon","family":"Avron","sequence":"first","affiliation":[]},{"given":"Furio","family":"Honsell","sequence":"additional","affiliation":[]},{"given":"Ian A.","family":"Mason","sequence":"additional","affiliation":[]},{"given":"Robert","family":"Pollack","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"Arnon Avron","year":"1991","unstructured":"AvronArnon, ?Simple consequence relations?, Information and Computation 92, 105?139 (1991).","journal-title":"Information and Computation"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(88)90037-0","volume":"57","author":"Arnon Avron","year":"1988","unstructured":"AvronArnon, ?The semantics and proof theory of linear logic?, Theoretical Computer Science 57, 161?184 (1988).","journal-title":"Theoretical Computer Science"},{"key":"CR3","unstructured":"Avron, Arnon, ?Modal logics in the Edinburgh LF?, in [4]."},{"key":"CR4","unstructured":"Avron, A., Harper, R., Honsell, F., Mason, I. and Plotkin, G. (Eds.), Workshop on General Logic-Edinburgh 1987. Technical Report, Laboratory for the Foundations of Computer Science, Edinburgh University (1988). ECS-LFCS-88-52."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Avron, A., Honsell, F. and I. Mason, ?An overview of the Edinburgh Logical Framework?, in: Current Trends in Hardware Verifications and Automated Theorem Proving. (Eds. G. Birtwistle and P. A. Subramanyam), Springer-Verlag (1989).","DOI":"10.1007\/978-1-4612-3658-0_8"},{"key":"CR6","unstructured":"Avron, A. and Honsell, F. and I. A. Mason, Using Typed Lambda Calculus to Implement Formal Systems on a Machine. Technical Report, Laboratory for Foundations of Computer Science, University of Edinburgh, ECS-LFCS-87-31 (1987)."},{"key":"CR7","unstructured":"Barendregt, H., The Lambda Calculus ? Its Syntax and Semantics, revised edition. North Holland (1984)."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H. Barringer","year":"1984","unstructured":"BarringerH., ChengJ. H. and JonesC. B., ?A logic covering undefinedness in program proofs?, Acta Informatics 21, 251?269 (1984).","journal-title":"Acta Informatics"},{"key":"CR9","unstructured":"de Bruijn, Nicolas G., ?A survey of the project AUTOMATH?, in: To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, Eds. J. P. Seldin and J. R. Hindley, pp. 589?606, Academic Press (1980)."},{"key":"CR10","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"Alonzo Church","year":"1940","unstructured":"ChurchAlonzo, ?A formulation of the simple theory of types?, J. Symbolic Logic 5, 56?68 (1940).","journal-title":"J. Symbolic Logic"},{"key":"CR11","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Robert L. Constable","year":"1986","unstructured":"ConstableRobert L. et al., Implementing Mathematics with the NuPRL Proof Development System, Prentice-Hall, Englewood Cliffs, NJ (1986)."},{"key":"CR12","unstructured":"Coquand, Thierry, Une th\u00e9orie des constructions, Th\u00e8se de Troisi\u00e8me Cycle, Universit\u00e9 Paris VII, January (1985)."},{"key":"CR13","unstructured":"Coquand, Thierry, Dowek, Gilles, Huet, G\u00e9rard and Paulin-Mohring, Christine, The Calculus of Constructions: Documentation and User's Guide. Projet Formel, INRIA-ENS, July (1989)."},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Coquand, Thierry and Huet, G\u00e9rard, ?Constructions: a higher-order proof system for mechanizing mathematics?, In EUROCAL '85: European Conference on Computer Algebra (ed. B. Buchberger), pp. 151?184, Springer-Verlag (1985).","DOI":"10.1007\/3-540-15983-5_13"},{"key":"CR15","first-page":"95","volume":"76","author":"Thierry Coquand","year":"1988","unstructured":"CoquandThierry and HuetG\u00e9rard, The calculus of constructions?, Information and Control 76, 95?120 (1988).","journal-title":"Information and Control"},{"key":"CR16","unstructured":"Fagin, R., Halpern, J. Y. and Vardi, M., ?What is an inference rule?? To appear in J. Symbolic Logic."},{"key":"CR17","unstructured":"Felty, Amy, Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language, Ph.D. thesis, University of Pennsylvania, August (1989)."},{"key":"CR18","unstructured":"Felty, Amy and Miller, Dale, ?Specifying theorem provers in a higher-order logic programming language?, in Ninth International Conference on Automated Deduction, Argonne, Il, May (1988)."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Felty, Amy and Miller, Dale, ?Encoding a dependent-type ?-calculus in a logic programming language?, in Tenth International Conference on Automated Deduction, Kaiserslautern, Germany, July (1990).","DOI":"10.1007\/3-540-52885-7_90"},{"key":"CR20","unstructured":"Dezani, Mariangiola, Honsell, Furio and Ronchi della Rocca, Simonetta, ?Models for theories of functions strictly depending on all their arguments?, J. Symbolic Logic 51(3) (1986) Abstract."},{"key":"CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"Jean-Yves Girard","year":"1987","unstructured":"GirardJean-Yves, ?Linear logic?, Theoretical Computer Science 50, 1 (1987).","journal-title":"Theoretical Computer Science"},{"key":"CR22","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation. Volume 78 of Lecture Notes in Computer Science","author":"Michael Gordon","year":"1979","unstructured":"GordonMichael, MilnerRobin and WadsworthChristopher, ?Edinburgh LCF: A Mechanized Logic of Computation. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, Heidelberg (1979)."},{"key":"CR23","unstructured":"Griffin, Timothy, An Environment for Formal Systems. Technical Report, Laboratory for the Foundations of Computer Science, Edinburgh University (1987) ECS-LFCS-87-34."},{"key":"CR24","unstructured":"Harper, Robert, Honsell, Furio and Plotkin, Gordon, ?A framework for defining logics, Proceedings of the Second Annual Symposium on Logic in Computer Science, Cornell (1987) (the full version will appear in J. ACM)."},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Huet, G. and Plotkin, G. (Eds.), Logical Frameworks, Cambridge University Press (1991).","DOI":"10.1017\/CBO9780511569807"},{"key":"CR26","unstructured":"Jutting, L. S., Checking Landau's Grundlagen in the AUTOMATH System. Ph.D. thesis, Eindhoven University, The Netherlands (1977)."},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"Kr\u00f6ger, Fred, Temporal Logic of Programs. Volume 8 of EATCS Monographs on Theoretical Computer Science, Springer-Verlag (1987).","DOI":"10.1007\/978-3-642-71549-5"},{"key":"CR28","doi-asserted-by":"crossref","unstructured":"Luo, Zhaohui, ?ECC, an extended calculus of constructions?, Proceedings of the Fourth Annual Symposium on Logic in Computer Science, Pacific Grove (1989).","DOI":"10.1109\/LICS.1989.39193"},{"key":"CR29","unstructured":"Luo, Zhaolui, Pollack, Robert and Taylor, Paul, ?How to use LEGO; A preliminary user's manual, Laboratory for the Foundations of Computer Science, Edinburgh University, April (1989)."},{"key":"CR30","first-page":"73","volume-title":"Logic Colloquium, '73","author":"Per Martin-L\u00f6f","year":"1973","unstructured":"Martin-L\u00f6fPer, ?An intuitionistic theory of types: predicative part?, in Logic Colloquium, '73 (H. E.Rose and J. C.Shepherdson, eds.), pp. 73?118, North-Holland, Amsterdam (1973)."},{"key":"CR31","unstructured":"Martin-L\u00f6f, Per, On the Meanings of the Logical Constants and the Justifications of the Logics Laws. Technical Report 2, Scuola di Specializzazione in Logica Matematics, Dipartimento di Matematics, Universit\u00e0 di Siena (1985)."},{"key":"CR32","unstructured":"Mason, Ian A., Hoare's Logic in the LF. Technical Report, Laboratory for the Foundations of Computer Science, Edinburgh University (1987). ECS-LFCS-87-32."},{"key":"CR33","unstructured":"Miller, Dale, Solutions to ?-Term Equations Under a Mixed Prefix. Unpublished draft, Department of Computer and Information Sciences, University of Pennsylvania, January (1989)."},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"Meyer, Albert and Reinhold, Mark, ??Type? is not a type: preliminary report?, in Proceedings of the 13th ACM Symposium on the Principles of Programming Languages (1986).","DOI":"10.1145\/512644.512671"},{"key":"CR35","volume-title":"An Introduction to Martin-L\u00f6f's Type Theory","author":"Bengt Nordstr\u00f6m","year":"1986","unstructured":"Nordstr\u00f6mBengt, PeterssonKent and SmithJan, An Introduction to Martin-L\u00f6f's Type Theory. University of G\u00f6teborg, G\u00f6teborg, Sweden (1986). Preprint."},{"key":"CR36","unstructured":"Ore, Christian-Emil, On Natural Deduction Style Semantics, Environments and Stores. Technical Report, Laboratory for the Foundations of Computer Science, Edinburgh University (1989). ECS-LFCS-89-88."},{"key":"CR37","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"Lawrence Paulson","year":"1986","unstructured":"PaulsonLawrence, ?Natural deduction proof as higher-order resolution?, J. Logic Programming 3, 237?258 (1986).","journal-title":"J. Logic Programming"},{"key":"CR38","unstructured":"Paulson, Lawrence, The Foundation of a Generic Theorem Prover. Technical Report 130, University of Cambridge Computer Laboratory, March (1988)."},{"key":"CR39","unstructured":"Petersson, Kent, A Programming System for Type Theory. Technical Report 21, Programming Methodology Group, University of G\u00f6teborg\/Chalmers Institute of Technology, March (1982)."},{"key":"CR40","doi-asserted-by":"crossref","unstructured":"Pfenning, Frank, Partial polymorphic type inference and higher-order unification?, Proceedings of the 1988 ACM Lips and Functional Programming Conference.","DOI":"10.1145\/62678.62697"},{"key":"CR41","doi-asserted-by":"crossref","unstructured":"Pfenning, Frank, ?ELf: A language for logic definition and verified metaprogramming?, Proceedings of the Fourth Annual Symposium on Logic in Computer Science, Pacific Grove (1989).","DOI":"10.1109\/LICS.1989.39186"},{"key":"CR42","doi-asserted-by":"crossref","unstructured":"Pfenning, Frank, ?Logic programming in the LF logical framework?, in [25].","DOI":"10.1017\/CBO9780511569807.008"},{"key":"CR43","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"Gordon Plotkin","year":"1975","unstructured":"PlotkinGordon, ?Call-by-name, call-by-value and the ?-calculus?, Theoretical Computer Science 1, 125?159 (1975).","journal-title":"Theoretical Computer Science"},{"key":"CR44","unstructured":"Pollack, Robert, The Theory of LEGO. Technical Report, Laboratory for the Foundations of Computer Science, Edinburgh University (1989). In preparation."},{"key":"CR45","volume-title":"Natural Deduction: A Proof-Theoretical Study","author":"Dag Prawitz","year":"1965","unstructured":"PrawitzDag, Natural Deduction: A Proof-Theoretical Study. Almquist & Wiksell, Stockholm (1965)."},{"key":"CR46","unstructured":"Pym, David, Proofs, Search and Computation in General Logic. Ph.D. Dissertation, University of Edinburgh, In Preparation (1989)."},{"key":"CR47","unstructured":"Pym, David and Wallen, Lincoln, Effective Search for the Logical Framework. Technical Report, Laboratory for the Foundations of Computer Science, Edinburgh University. In preparation (1989)."},{"key":"CR48","doi-asserted-by":"crossref","unstructured":"Reynolds, J. C., ?Syntactic control of Interference?, Conference Record of the Fifth Annual Symposium on Principles of Programming Languages, Tucson (1978).","DOI":"10.1145\/512760.512766"},{"key":"CR49","unstructured":"Salvesen, Anne, ?A proof of the Church-Rosser property for the Edinburgh LF with eta-conversion?, Proceedings of the first Workshop on Logical Frameworks, Sophia Antipolis (1990)."},{"key":"CR50","volume-title":"Mathematical Logic","author":"Joseph R. Schoenfield","year":"1967","unstructured":"SchoenfieldJoseph R., Mathematical Logic, Addison-Wesley, Reading, Massachusetts (1967)."},{"key":"CR51","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","volume":"49","author":"Colin Stirling","year":"1987","unstructured":"StirlingColin, ?Modal logics for communicating systems?, Theoretical Computer Science 49, 311?347 (1987).","journal-title":"Theoretical Computer Science"},{"key":"CR52","unstructured":"Taylor, Paul, Playing with LEGO: Some Examples of Developing Mathematics in the Calculus of Constructions. Technical Report, Laboratory for the Foundations of Computer Science, Edinburgh University (1989). ECS-LFCS-89-89."},{"key":"CR53","unstructured":"Weis, Pierre et al., The CAML Reference Manual, Version 2.6, Projet Formel, INRIA-ENS, March (1989)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00245294.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00245294\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00245294","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T21:43:44Z","timestamp":1585950224000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00245294"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,12]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1992,12]]}},"alternative-id":["BF00245294"],"URL":"https:\/\/doi.org\/10.1007\/bf00245294","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,12]]}}}