{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:56Z","timestamp":1749125156389},"publisher-location":"Berlin\/Heidelberg","reference-count":20,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540582770"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0049326","type":"book-chapter","created":{"date-parts":[[2006,3,6]],"date-time":"2006-03-06T18:58:16Z","timestamp":1141671496000},"page":"91-105","source":"Crossref","is-referenced-by-count":14,"title":["From semantics to rules: A machine assisted analysis"],"prefix":"10.1007","author":[{"given":"Catarina","family":"Coquand","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Cardelli, P-L. Curien and J-J L\u00e9vy. Explicit Substitutions. ACM Conference on Principles of Programming Languages, San Francisco, 1990.","DOI":"10.1145\/96709.96712"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed \u03bb-calculus. Proceedings of LICS 91.","DOI":"10.1109\/LICS.1991.151645"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"U. Berger. Program extraction from normalization proofs. Proceedings of TLCA'93, LNCS vol. 664","DOI":"10.1007\/BFb0037100"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen, Th. Coquand, C.A. Gunter and A. Scedrov. Inheritance as implicit coercion. Logic and Computation, feb 1991.","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"7_CR5","unstructured":"C. Coquand Analysis of simply typed lambda-calculus in ALF. Proceedings of the Winter Meeting, Tanum Strand, 1993."},{"key":"7_CR6","unstructured":"Th. Coquand and P. Dybjer. Intuitionistic Model Constructions and Normalization Proofs. Paper in preparation."},{"key":"7_CR7","unstructured":"Th. Coquand and J. Gallier. A proof of strong normalization for the theory of constructions using a Kripke-like interpretation. Proceedings of the first workshop in Logical Frameworks."},{"key":"7_CR8","unstructured":"Th. Coquand. Pattern Matching with Dependent Types. Proceedings of the 1992 Workshop on Types for Proofs and Programs, eds B. Nordstr\u00f6m, K. Petersson and G. Plotkin."},{"key":"7_CR9","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2268484","volume":"21","author":"R. O. Gandy","year":"1956","unstructured":"R. O. Gandy. On the Axiom of Extensionality \u2014 Part I. The Journal of symbolic logic, volume 21, March 1956, p 36\u201348.","journal-title":"The Journal of symbolic logic"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"S. A. Kripke Semantical analysis of intutionistic logic 1 Formal systems and recursive functions, 1965, eds J.N. Crossley and M.A.E. Dummet, North-Holland.","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"7_CR11","unstructured":"L. Magnusson. The new implementation of ALF. Proceedings of the 1992 Workshop on Types for Proofs and Programs, eds B. Nordstr\u00f6m, K. Petersson and G. Plotkin."},{"key":"7_CR12","unstructured":"P. Martin-L\u00f6f. Substitution calculus. Handwritten notes, G\u00f6teborg, 1992."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. An Intuitionistic Theory of Types: Predicative Part. Logic Colloquium '73, 1975, p. 73\u2013118, eds. H. E. Rose and J. C. Shepherdson, North-Holland.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell and E. Moggi. Kripke-style models for typed lambda calculus. Annals for Pure and Applied Logic 51, 1991, p 99\u2013124, North-Holland.","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"7_CR15","unstructured":"B. Nordstr\u00f6m, K. Petersson and J. Smith. Programming in Martin-L\u00f6f's Type Theory. An Introduction. Oxford University Press, 1990."},{"key":"7_CR16","unstructured":"Eike Ritter. Categorical abstract machine for higher-order typed \u03bb-calculus. Phd thesis, Univ. of Cambridge, 30 Sept, 1992."},{"key":"7_CR17","unstructured":"Dana S. Scott. Relating theories of the lambda-calculus. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, 1980."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"R. Statman. Logical Relation and the Typed \u03bb-calculus. Information and Control, 65, 1985.","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"7_CR19","unstructured":"A. Tasistro. Formulation of Martin-L\u00f6f's theory of types with explicit substitutions. Licentiate thesis, 1993."},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"R.D. Tennant. Semantical analysis of specification logic. Logics of programs. LNCS, vol. 193 Springer, 1985, p.373\u2013386.","DOI":"10.1007\/3-540-15648-8_28"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0049326.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:55:40Z","timestamp":1607550940000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0049326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540582770"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0049326","relation":{},"subject":[]}}