{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:10Z","timestamp":1774837810135,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540314288","type":"print"},{"value":"9783540314295","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11617990_10","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T11:39:40Z","timestamp":1137670780000},"page":"154-169","source":"Crossref","is-referenced-by-count":17,"title":["A Tool for Automated Theorem Proving in Agda"],"prefix":"10.1007","author":[{"given":"Fredrik","family":"Lindblad","sequence":"first","affiliation":[]},{"given":"Marcin","family":"Benke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A., Coquand, T., Norell, U.: Connecting a logical framework to a first-order logic prover (2005) (submitted)","DOI":"10.1007\/11559306_17"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1016\/B978-044450813-3\/50017-5","volume-title":"Handbook of Automated Reasoning","author":"P.B. Andrews","year":"2001","unstructured":"Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, ch. 15, pp. 965\u20131007. Elsevier Science, Amsterdam (2001)"},{"key":"10_CR3","unstructured":"Coquand, C.: The AGDA Proof System Homepage (1998), https:\/\/linproxy.fan.workers.dev:443\/http\/www.cs.chalmers.se\/~catarina\/agda\/"},{"key":"10_CR4","unstructured":"Cornes, C.: Conception d\u2019un langage de haut niveau de repr\u00e9sentation de preuves: R\u00e9currence par filtrage de motifs, Unification en pr\u00e9sence de types inductifs primitifs, Synth\u00e8se de lemmes d\u2019inversion. PhD thesis, Universit\u00e9 Paris 7 (1997)"},{"issue":"3","key":"10_CR5","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1093\/logcom\/3.3.287","volume":"3","author":"G. Dowek","year":"1993","unstructured":"Dowek, G.: A complete proof synthesis method for the cube of type systems. J. Logic and Computation\u00a03(3), 287\u2013315 (1993)","journal-title":"J. Logic and Computation"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"1009","DOI":"10.1016\/B978-044450813-3\/50018-7","volume-title":"Handbook of automated reasoning","author":"G. Dowek","year":"2001","unstructured":"Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of automated reasoning, vol.\u00a02, ch. 16, pp. 1009\u20131062. Elsevier Science, Amsterdam (2001)"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1017\/CBO9780511569807.012","volume-title":"Logical frameworks","author":"P. Dybjer","year":"1991","unstructured":"Dybjer, P.: Inductive sets and families in martin-l\u00f6f\u2019s type theory and their set-theoretic semantics. In: Logical frameworks, pp. 280\u2013306. Cambridge University Press, New York (1991)"},{"key":"10_CR8","unstructured":"Lindblad, F.: Agsy problem examples (2004), https:\/\/linproxy.fan.workers.dev:443\/http\/www.cs.chalmers.se\/~frelindb\/Agsy_examples.tgz"},{"key":"10_CR9","unstructured":"Magnusson, L.: The Implementation of ALF - a Proof Editor based on Martin-L\u00f6f\u2019s Monomorphic Type Theory with Explicit Substitution. PhD thesis, Department of Computing Science, Chalmers University of Technology and University of G\u00f6teborg (1994)"},{"key":"10_CR10","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis, Napoli (1984)"},{"key":"10_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/BFb0054266","volume-title":"Automated Deduction - CADE-15","author":"C. Sch\u00fcrmann","year":"1998","unstructured":"Sch\u00fcrmann, C., Pfenning, F.: Automated theorem proving in a simple meta-logic for LF. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 286\u2013300. Springer, Heidelberg (1998)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Tammet, T., Smith, J.: Optimized encodings of fragments of type theory in first-order logic. Journal of Logic and Computation\u00a08 (1998)","DOI":"10.1093\/logcom\/8.6.713"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/link.springer.com\/content\/pdf\/10.1007\/11617990_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:04:02Z","timestamp":1605643442000},"score":1,"resource":{"primary":{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/link.springer.com\/10.1007\/11617990_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540314288","9783540314295"],"references-count":12,"URL":"https:\/\/linproxy.fan.workers.dev:443\/https\/doi.org\/10.1007\/11617990_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}