{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:34:43Z","timestamp":1725489283660},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540741299"},{"type":"electronic","value":"9783540741305"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74130-5_9","type":"book-chapter","created":{"date-parts":[[2007,8,13]],"date-time":"2007-08-13T11:32:56Z","timestamp":1187004776000},"page":"145-162","source":"Crossref","is-referenced-by-count":1,"title":["Ivor, a Proof Engine"],"prefix":"10.1007","author":[{"given":"Edwin","family":"Brady","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Cover translator. http:\/\/coverproject.org\/CoverTranslator\/","key":"9_CR1"},{"unstructured":"Barras, B., Werner, B.: Coq in Coq (1997)","key":"9_CR2"},{"unstructured":"Brady, E.: Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, University of Durham (2005)","key":"9_CR3"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/11964681_5","volume-title":"Implementation and Application of Functional Languages","author":"E. Brady","year":"2006","unstructured":"Brady, E., Hammond, K.: A dependently typed framework for static analysis of program execution costs. In: Butterfield, A., Grelck, C., Huch, F. (eds.) IFL 2005. LNCS, vol.\u00a04015, pp. 74\u201390. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Brady, E., Hammond, K.: A verified staged interpreter is a verified compiler. In: Proc. Conf. Generative Programming and Component Engineering (GPCE\u00a02006) (2006)","key":"9_CR5","DOI":"10.1145\/1173706.1173724"},{"unstructured":"Chapman, J., Altenkirch, T., McBride, C.: Epigram reloaded: A standalone typechecker for ETT. In: Trends in Functional Programming, 2005 (to appear)","key":"9_CR6"},{"unstructured":"Coq Development Team. The Coq proof assistant \u2014 reference manual (2001), http:\/\/coq.inria.fr\/","key":"9_CR7"},{"unstructured":"Coquand, C.: Agda (2005), http:\/\/agda.sourceforge.net\/","key":"9_CR8"},{"unstructured":"Coquand, T.: Pattern matching with dependent types (1992), Available from http:\/\/www.cs.chalmers.se\/~coquand\/type.html","key":"9_CR9"},{"key":"9_CR10","volume-title":"Combinatory Logic","author":"H.B. Curry","year":"1958","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic, vol.\u00a01. North Holland, Amsterdam (1958)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46028-4_4","volume-title":"Implementation of Functional Languages","author":"M. Mol de","year":"2002","unstructured":"de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem proving for functional programmers. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol.\u00a02312, Springer, Heidelberg (2002)"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive families. Formal Aspects Of Computing\u00a06, 440\u2013465 (1994)","journal-title":"Formal Aspects Of Computing"},{"unstructured":"Filli\u00e2tre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud (March 2003)","key":"9_CR13"},{"doi-asserted-by":"crossref","unstructured":"Geuvers, H., Wiedijk, F., Zwanenburg, J.: A constructive proof of the fundamental theorem of algebra without using the rationals. In: TYPES 2000, pp. 96\u2013111 (2000)","key":"9_CR14","DOI":"10.1007\/3-540-45842-5_7"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-61780-9_67","volume-title":"Types for Proofs and Programs","author":"E. Gim\u00e9nez","year":"1996","unstructured":"Gim\u00e9nez, E.: An application of co-inductive types in coq: Verification of the alternating bit protocol. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 135\u2013152. Springer, Heidelberg (1996)"},{"unstructured":"Gonthier, G.: A computer-checked proof of the Four Colour Theorem (2005), http:\/\/research.microsoft.com\/~gonthier\/4colproof.pdf","key":"9_CR16"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Generative Programming and Component Engineering","author":"K. Hammond","year":"2003","unstructured":"Hammond, K., Michaelson, G.: Hume: a Domain-Specific Language for Real-Time Embedded Systems. In: Pfenning, F., Smaragdakis, Y. (eds.) GPCE 2003. LNCS, vol.\u00a02830, Springer, Heidelberg (2003)"},{"key":"9_CR18","volume-title":"To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A.: The formulae-as-types notion of construction, A reprint of an unpublished manuscript from 1969. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism, Academic Press, San Diego (1980)"},{"doi-asserted-by":"crossref","unstructured":"Hudak, P.: Building domain-specific embedded languages. ACM Computing Surveys, 28A(4) (December 1996)","key":"9_CR19","DOI":"10.1145\/242224.242477"},{"key":"9_CR20","first-page":"42","volume-title":"Principles of Programming Languages 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end. In: Principles of Programming Languages 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Types for proofs and programs","author":"P. Letouzey","year":"2002","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) Types for proofs and programs. LNCS, Springer, Heidelberg (2002)"},{"unstructured":"Luo, Z.: Computation and Reasoning \u2013 A Type Theory for Computer Science. Intl. Series of Monographs on Comp. Sci. OUP (1994)","key":"9_CR22"},{"unstructured":"Luo, Z., Pollack, R.: Lego proof development system: User\u2019s manual. Technical report, Department of Computer Science, University of Edinburgh (1992)","key":"9_CR23"},{"unstructured":"McBride, C.: Dependently Typed Functional Programs and their proofs. PhD thesis, University of Edinburgh (May 2000)","key":"9_CR24"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_12","volume-title":"Types for Proofs and Programs","author":"C. McBride","year":"2006","unstructured":"McBride, C., Goguen, H., McKinna, J.: Some constructions on constructors. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, Springer, Heidelberg (2006)"},{"unstructured":"McBride, C., McKinna, J.: I am not a number, I am a free variable. In: Proceedings of the ACM SIGPLAN Haskell Workshop (2004)","key":"9_CR26"},{"issue":"1","key":"9_CR27","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming\u00a014(1), 69\u2013111 (2004)","journal-title":"Journal of Functional Programming"},{"unstructured":"McKinna, J., Wright, J.: A type-correct, stack-safe, provably correct, expression compiler in Epigram. Journal of Functional Programming (to appear, 2007)","key":"9_CR28"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","first-page":"146","volume-title":"Mathematical Foundations of Computer Science 1978","author":"R. Milner","year":"1978","unstructured":"Milner, R.: LCF: A way of doing proofs with a machine. In: Winkowski, J. (ed.) Mathematical Foundations of Computer Science 1978. LNCS, vol.\u00a064, pp. 146\u2013159. Springer, Heidelberg (1978)"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A proof assistant for higher order logic. In: Nipkow, T., Paulson, L.C., Wenzel, M. (eds.) Isabelle\/HOL. LNCS, vol.\u00a02283, Springer, Heidelberg (2002)"},{"unstructured":"Jones, S.P., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Proc. 2006 International Conf. on Functional Programming (ICFP 2006) (2006)","key":"9_CR31"},{"unstructured":"Plasmeijer, R., van Eekelen, M.: The Concurrent CLEAN language report (draft) (2003), Available from http:\/\/www.cs.kun.nl\/~clean\/","key":"9_CR32"},{"unstructured":"Pollack, R.: Implicit syntax. Informal Proceedings of First Workshop on Logical Frameworks, Antibes (May 1990)","key":"9_CR33"},{"doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega Test: a fast and practical integer programming algorithm for dependence analysis. Communication of the ACM, pp. 102\u2013114 (1992)","key":"9_CR34","DOI":"10.1145\/135226.135233"},{"doi-asserted-by":"crossref","unstructured":"Sheard, T.: Languages of the future. In: ACM Conference on Object Orientated Programming Systems, Languages and Applicatioons (OOPSLA 2004) (2004)","key":"9_CR35","DOI":"10.1145\/1028664.1028711"},{"doi-asserted-by":"crossref","unstructured":"Taha, W.: A gentle introduction to multi-stage programming (2003), Available from http:\/\/www.cs.rice.edu\/~taha\/publications\/journal\/dspg04a.pdf","key":"9_CR36","DOI":"10.1007\/978-3-540-25935-0_3"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Functional Languages"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74130-5_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:11:50Z","timestamp":1619503910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74130-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540741299","9783540741305"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74130-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}