{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T07:40:25Z","timestamp":1743579625560,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642311123"},{"type":"electronic","value":"9783642311130"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31113-0_12","type":"book-chapter","created":{"date-parts":[[2012,6,20]],"date-time":"2012-06-20T05:04:11Z","timestamp":1340168651000},"page":"220-240","source":"Crossref","is-referenced-by-count":1,"title":["Dependently Typed Programming Based on Automated Theorem Proving"],"prefix":"10.1007","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[]},{"given":"Simon","family":"Foster","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M. Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Armstrong, A., Struth, G., Foster, S.: Dependently typed programming based on automated theorem proving. Technical Report (2011), http:\/\/arxiv.org\/abs\/1112.3833","DOI":"10.1007\/978-3-642-31113-0_12"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General: A Generic Tool for Proof Development. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, pp. 38\u201342. Springer, Heidelberg (2000)"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1017\/S0305004108001783","volume":"146","author":"S. Awodey","year":"2009","unstructured":"Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. Camb. Phil. Soc.\u00a0146, 45\u201355 (2009)","journal-title":"Math. Proc. Camb. Phil. Soc."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Ait-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, pp. 1\u201330. Academic Press (1989)","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"issue":"2","key":"12_CR6","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"Barendregt, H.: Introduction to generalized type systems. Journal of functional programming\u00a01(2), 125\u2013154 (1991)","journal-title":"Journal of functional programming"},{"issue":"3","key":"12_CR7","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. Journal of Automated Reasoning\u00a028(3), 321\u2013336 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/1932681.1863592","volume":"45","author":"J.-P. Bernardy","year":"2010","unstructured":"Bernardy, J.-P., Jansson, P., Paterson, R.: Parametricity and dependent types. SIGPLAN Not.\u00a045, 345\u2013356 (2010)","journal-title":"SIGPLAN Not."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos 2011. LNCS, vol.\u00a06989, pp. 12\u201327. Springer, Heidelberg (2011)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A Brief Overview of Agda \u2013 A Functional Language with Dependent Types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 73\u201378. Springer, Heidelberg (2009)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-28729-9_7","volume-title":"Foundations of Software Science and Computational Structures","author":"A. Bove","year":"2012","unstructured":"Bove, A., Dybjer, P., Sicard-Ram\u00edrez, A.: Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol.\u00a07213, pp. 104\u2013118. Springer, Heidelberg (2012)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. Journal of Automated Reasoning (2011), doi:10.1007\/s10817-011-9225-2","DOI":"10.1007\/s10817-011-9225-2"},{"key":"12_CR14","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"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-20398-5_10","volume-title":"NASA Formal Methods","author":"S. Foster","year":"2011","unstructured":"Foster, S., Struth, G.: Integrating an Automated Theorem Prover into Agda. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP 2011, pp. 163\u2013175. ACM (2011)","DOI":"10.1145\/2034574.2034798"},{"key":"12_CR17","unstructured":"PRL Group. Implementing Mathematics with the Nuprl Proof Development System. Computer Science Department, Cornell University (1995), http:\/\/www.cs.cornell.edu\/info\/projects\/nuprl\/book\/doc.html"},{"issue":"2","key":"12_CR18","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T. Hillenbrand","year":"1997","unstructured":"Hillenbrand, T., Buch, A., Vogt, R., L\u00f6chner, B.: Waldmeister: High performance equational deduction. Journal of Automated Reasoning\u00a018(2), 265\u2013270 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR19","unstructured":"Hurd, J.: System description: The Metis proof tactic. In: Benzm\u00fcller, C., Harrison, J., Sch\u00fcrmann, D. (eds.) ESHOL 2005, pp. 103\u2013104 (2005), arXiv.org"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"L\u00f6h, A., McBride, C., Swierstra, W.: A Tutorial Implementation of a Dependently Typed Lambda Calculus. In: Altenkirch, T., Uustalu, T. (eds.) Dependently Typed Programming. Fundamenta Informaticae, vol.\u00a0102(2), pp. 177\u2013207. IOS Press (2010)","DOI":"10.3233\/FI-2010-304"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/11546382_3","volume-title":"Advanced Functional Programming","author":"C. McBride","year":"2005","unstructured":"McBride, C.: Epigram: Practical Programming with Dependent Types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol.\u00a03622, pp. 130\u2013170. Springer, Heidelberg (2005)"},{"key":"12_CR23","unstructured":"Miquel, A.: Le calcul des constructions implicite: syntaxe et s\u00e9mantique. These de doctorat, Universit\u00e9 Paris, 7 (2001)"},{"key":"12_CR24","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction","author":"B. Nordstrom","year":"1990","unstructured":"Nordstrom, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Oxford University Press, USA (1990)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U. Norell","year":"2009","unstructured":"Norell, U.: Dependently Typed Programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol.\u00a05832, pp. 230\u2013266. Springer, Heidelberg (2009)"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Pierce, B.C. (ed.): Advanced topics in types and programming languages. The MIT Press (2005)","DOI":"10.7551\/mitpress\/1104.001.0001"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Pierce, B.C., Turner, D.N.: Local Type Inference. In: Pugh, W. (ed.) TOPLAS 2000, pp. 1\u201344. ACM (2000)","DOI":"10.1145\/345099.345100"},{"key":"12_CR28","unstructured":"Pierce, B.C.: Types and programming languages. The MIT Press (2002)"},{"key":"12_CR29","unstructured":"Rudnicki, P., Urban, J.: Escape to ATP in Mizar. PxTP 2011 (2011)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Rushby, J.M.: Tutorial: Automated formal methods with PVS, SAL and Yices. In: Hung, D.V., Pandya, P. (eds.) SEFM 2006, p. 262. IEEE Press (2006)","DOI":"10.1109\/SEFM.2006.37"},{"issue":"4","key":"12_CR31","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR32","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) FroCoS 2004, pp. 201\u2013215. IOS Press (2004)"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31113-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T07:27:53Z","timestamp":1743578873000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-31113-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642311123","9783642311130"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31113-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}