{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:46Z","timestamp":1725456226906},"publisher-location":"Berlin\/Heidelberg","reference-count":8,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012875","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"740-741","source":"Crossref","is-referenced-by-count":0,"title":["EFS \u2014 An interactive Environment for Formal Systems"],"prefix":"10.1007","author":[{"given":"Timothy G.","family":"Griffin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"56_CR1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"Robert L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"56_CR2","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and G\u00e9rard Huet. Constuctions: a higher order proof system for mechanizing mathematics. In Bruno Buchberger, editor, EUROCAL '85, pages 151\u2013184, Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"56_CR3","unstructured":"N. G. de Bruijn. A survey of the project AUTOMATH. In J. P. Seldin and J. R. Hindley, editors, Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589\u2013606, Academic Press, 1980."},{"key":"56_CR4","unstructured":"Timothy G. Griffin. An Environment for Formal Systems. Technical Report 87-846, Department of Computer Science, Cornell University, 1987. (also LFCS report ECS-LFCS-87-34, Department of Computer Science, University of Edinburgh)."},{"key":"56_CR5","doi-asserted-by":"crossref","unstructured":"Timothy G. Griffin. Notational definitions \u2014 a formal account. In Proceedings of the Third Symposium on Logic in Computer Science, July 1988. To appear.","DOI":"10.1109\/LICS.1988.5134"},{"key":"56_CR6","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Proceedings of the Second Symposium on Logic in Computer Science, 1987."},{"key":"56_CR7","doi-asserted-by":"crossref","unstructured":"Thomas W. Reps and Bowen Alpern. Interactive proof checking. In POPL11, 1984.","DOI":"10.1145\/800017.800514"},{"key":"56_CR8","volume-title":"The Synthesizer Generator Reference Manual","author":"T. W. Reps","year":"1987","unstructured":"Thomas W. Reps and T. Teitelbaum. The Synthesizer Generator Reference Manual. Dept. of Computer Science, Cornell University, Ithaca, NY,14853, 1985. Second Edition, 1987.","edition":"Second Edition"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012875.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:48Z","timestamp":1607353608000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/bfb0012875","relation":{},"subject":[]}}