{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,3]],"date-time":"2024-02-03T00:40:12Z","timestamp":1706920812078},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2005,7,1]],"date-time":"2005-07-01T00:00:00Z","timestamp":1120176000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2005,7]]},"DOI":"10.1007\/s11390-005-0526-y","type":"journal-article","created":{"date-parts":[[2006,2,17]],"date-time":"2006-02-17T08:47:07Z","timestamp":1140166027000},"page":"526-535","source":"Crossref","is-referenced-by-count":0,"title":["LFTOP: An LF-Based Approach to Domain-Specific Reasoning"],"prefix":"10.1007","volume":"20","author":[{"given":"Jian-Min","family":"Pang","sequence":"first","affiliation":[]},{"given":"Paul","family":"Callaghan","sequence":"additional","affiliation":[]},{"given":"Zhao-Hui","family":"Luo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"526_CR1","doi-asserted-by":"crossref","unstructured":"Luo Z. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"526_CR2","unstructured":"Milner R. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. SU Fisher Research 511\/24."},{"key":"526_CR3","unstructured":"Milner R. Communicating and Mobile Systems: The Pi-Calculus. Springer Verlag, ISBN 0521658691, 1999."},{"issue":"3","key":"526_CR4","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"December 1983","unstructured":"Kozen D. Results on the propositional \u03bc-calculus. Theoretical Computer Science, December 1983, 27(3): 333\u2013354.","journal-title":"Theoretical Computer Science"},{"key":"526_CR5","unstructured":"Callaghan P C, Luo Z, Pang J. Object languages in a type theoretic meta-framework. In Proc. Workshop on Proof Transformation, Presentation and Proof Complexities, Siena, Italy, June 19, 2001, pp.23\u201336."},{"key":"526_CR6","unstructured":"Howard W. The Formulae-as-Type Notion of Construction. To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, Seldin J, Hindley J (eds.), Academic Press, 1980."},{"issue":"1","key":"526_CR7","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/BF02948849","volume":"16","author":"Yuxi Fu","year":"2001","unstructured":"Fu Yuxi. Semantics of constructions (I) \u2014 The traditional approach. Journal of Computer Science and Technology, 2001, 16(1): 13\u201324.","journal-title":"Journal of Computer Science and Technology"},{"issue":"1","key":"526_CR8","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"McBride Conor","year":"2004","unstructured":"Conor McBride, James McKinna. The view from the left. Journal of Functional Programming, 2004, 14(1): 69\u2013111.","journal-title":"Journal of Functional Programming"},{"key":"526_CR9","unstructured":"Callaghan P C, Luo Z. Plastic: An implementation of typed LF with coercive subtyping and universes. J. Automated Reasoning, Special Issue on Logical Frameworks, 2000."},{"key":"526_CR10","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 7.3 1. http:\/\/pauillac.inria.fr\/coq\/doc\/main.html."},{"key":"526_CR11","unstructured":"Pollack R. Lego WWW page. http:\/\/www.dcs.ed.ac.uk\/home\/lego."},{"key":"526_CR12","doi-asserted-by":"crossref","unstructured":"Paulson L C. Isabelle: A generic theorem prover. Lecture Notes in Computer Science 828: xvii + 321, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"526_CR13","unstructured":"Isabelle. Isabelle WWW Page. http:\/\/www.cl.cam.ac.uk\/Re-se-arch\/HVG\/Isabelle"},{"key":"526_CR14","unstructured":"Markus M Wenzel. Isabelle\/Isar \u2013 A versatile environment for human-readable formal proof documents [Dissertation]. TU M\u00fcnchen, 2002."},{"key":"526_CR15","unstructured":"Yu S. Verification of concurrent programs based on type theory [Dissertation]. University of Durham, 1999."},{"key":"526_CR16","doi-asserted-by":"crossref","unstructured":"Shenwei Yu, Zhaohui Luo. Implementing a model checker for LEGO. In FME'97: Industrial Applications and Strengthened Foundations of Formal Methods (Proc. 4th Int. Symposium of Formal Methods Europe), John Fitzgerald, Cliff B Jones, Peter Lucas (eds.), 1997, LNCS 1313, pp.442\u2013458.","DOI":"10.1007\/3-540-63533-5_23"},{"key":"526_CR17","doi-asserted-by":"crossref","unstructured":"Sam Owre, John Rushby, Shankar N. Integration in PVS: Tables, types, and model checking. In Tools and Algorithms for the Construction and Analysis of Systems TACAS'97, Brinksma (ed.), Lecture Notes in Computer Science 1217, Enschede, The Netherlands, April 1997, Springer-Verlag, pp.366\u2013383.","DOI":"10.1007\/BFb0035400"},{"key":"526_CR18","doi-asserted-by":"crossref","unstructured":"Archer M, Heitmeyer C. Human-style theorem proving using PVS. In Proc. 10th Int. Theorem Proving in Higher Order Logics, 1997, pp.33\u201348.","DOI":"10.21236\/ADA464276"},{"key":"526_CR19","unstructured":"Mark Saaltink. The Z\/EVES user's guide. Technical Report TR-97-5493-06, ORA Canada, September 1997."},{"key":"526_CR20","unstructured":"Martin Leucker, Thomas Noll. Truth \u2013 A real-world application in haskell. In Proc. the 12th International Workshop on Implementation of Functional Languages (IFL'00), Markus Mohnen (ed.), number AIB-00-7 in Aachener Informatik Berichte, RWTH Aachen, September 2000, pp.363\u2013380."},{"key":"526_CR21","unstructured":"Igor Walukiewicz. A complete deductive system for the \u03bc-calculus [Dissertation]. Warsaw University, 1993."},{"key":"526_CR22","doi-asserted-by":"crossref","unstructured":"Healfdene Goguen. Soundness of the logical framework for its typed operational semantics. In Proc. 4th Intl. Conf. Typed Lambda Calculi & Applications (TLCA'99), Girard J Y (ed.), L'Aquila, Italy, 1999, pp.177\u2013197.","DOI":"10.1007\/3-540-48959-2_14"},{"issue":"1","key":"526_CR23","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"Cleaveland Rance","year":"January 1993","unstructured":"Rance Cleaveland, Joachim Parrow, Bernhard Steffen. The concurrency workbench: A semantics-based tool for the verification of concurrent systems. ACM Trans. Programming Languages and Systems, January 1993, 15(1): 36\u201372.","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"526_CR24","unstructured":"Henk Barendregt et al. The \u201cFundamental Theorem of Algebra\u201d Project. http:\/\/www.cs.kun.nl\/~freek\/fta\/xindex.html"},{"key":"526_CR25","unstructured":"Bertot Y, Kleymann-Schreiber T, Sequeira D. Implementing proof by pointing without a structure editor. Technical Report ECS-LFCS-97-368. Dept. Computer Science, University of Edinburgh, 1997."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-005-0526-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-005-0526-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-005-0526-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,3]],"date-time":"2024-02-03T00:23:09Z","timestamp":1706919789000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-005-0526-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["526"],"URL":"https:\/\/doi.org\/10.1007\/s11390-005-0526-y","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,7]]}}}