{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:15Z","timestamp":1725474495271},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097793","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T09:27:48Z","timestamp":1164360468000},"page":"196-215","source":"Crossref","is-referenced-by-count":0,"title":["Semantical BNF"],"prefix":"10.1007","author":[{"given":"Petri","family":"M\u00e4enp\u00e4\u00e4","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"11_CR1","volume-title":"Compilers, Principles, Techniques, and Tools","author":"A. V. Aho","year":"1986","unstructured":"Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers, Principles, Techniques, and Tools. Addison-Wesley, Reading, Massachusetts, 1986."},{"key":"11_CR2","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. Bruijn de","year":"1972","unstructured":"N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381\u2013392, 1972. Reprinted in R. Nederpelt et al., editors, Selected Papers on Automath, pages 865\u2013935. North-Holland, Amsterdam, 1994.","journal-title":"Indagationes Mathematicae"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/BFb0014049","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications","author":"J. Despeyroux","year":"1995","unstructured":"Jo\u00eblle Despeyroux, Amy Felty, and Andr\u00e9 Hirschowitz. Higher-order abstract syntax in Coq. In M. Dezani and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 124\u2013138. Lecture Notes in Computer Science 902, Springer-Verlag, Heidelberg, 1995."},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF01692511","volume":"2","author":"D. E. Knuth","year":"1968","unstructured":"Donald E. Knuth. Semantics of context-free languages. Mathematical Systems Theory, 2:127\u2013145, 1968. Errata 5:95\u201396, 1971.","journal-title":"Mathematical Systems Theory"},{"key":"11_CR5","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/BFb0059699","volume-title":"Symposium on Semantics of Algorithmic Languages","author":"D. E. Knuth","year":"1971","unstructured":"Donald E. Knuth. Examples of formal semantics. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages, pages 212\u2013235. Lecture Notes in Mathematics 188, Springer-Verlag, Heidelberg, 1971."},{"key":"11_CR6","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, Naples, 1984."},{"key":"11_CR7","volume-title":"Formal Philosophy","author":"R. Montague","year":"1974","unstructured":"Richard Montague. Formal Philosophy Collected papers edited by Richmond Thomason. Yale University Press, New Haven, 1974."},{"key":"11_CR8","volume-title":"Type Theoretical Grammar","author":"A. Ranta","year":"1994","unstructured":"Aarne Ranta. Type Theoretical Grammar. Oxford University Press, Oxford, 1994."},{"key":"11_CR9","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1093\/jigpal\/3.2-3.319","volume":"3","author":"A. Ranta","year":"1995","unstructured":"Aarne Ranta. Type-theoretical interpretation and generalization of phrase structure grammar. Bulletin of the IGPL, 3:319\u2013342, 1995a.","journal-title":"Bulletin of the IGPL"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-60579-7_9","volume-title":"Types for Proofs and Programs","author":"A. Ranta","year":"1995","unstructured":"Aarne Ranta. Syntactic categories in the language of mathematics. In P. Dybjer, B. Nordstr\u00f6m, and J. Smith, editors, Types for Proofs and Programs, pages 162\u2013182. Lecture Notes in Computer Science 996, Springer-Verlag, Heidelberg, 1995b."},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","first-page":"162","volume-title":"Types for Proofs and Programs","author":"A. Ranta","year":"1996","unstructured":"Aarne Ranta. Context-dependent syntactic categories and the formalization of mathematical text. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, pages 162\u2013182. Lecture Notes in Computer Science 1158, Springer-Verlag, Heidelberg, 1996."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Aarne Ranta. Structures grammaticales dans le fran\u00e7ais math\u00e9matique. To appear in Math\u00e9matiques Informatique, Sciences humaines, 1997.","DOI":"10.4000\/msh.2772"},{"key":"11_CR13","volume-title":"The Structure of Typed Programming Languages","author":"D. A. Schmidt","year":"1994","unstructured":"David A. Schmidt. The Structure of Typed Programming Languages. MIT Press, Massachusetts, 1994."},{"key":"11_CR14","unstructured":"Alvaro Tasistro. Formulation of Martin-L\u00f6f's theory of types with explicit substitutions. Licentiate's thesis, Chalmers University of Technology and University of G\u00f6teborg, 1993."},{"key":"11_CR15","volume-title":"Semantics of Programming Languages","author":"R. D. Tennent","year":"1991","unstructured":"R. D. Tennent. Semantics of Programming Languages. Prentice Hall, New York, 1991."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T10:53:56Z","timestamp":1555930436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097793"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0097793","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}