{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T12:49:12Z","timestamp":1790945352296,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,9,21]],"date-time":"2008-09-21T00:00:00Z","timestamp":1221955200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2008,9,21]]},"DOI":"10.1145\/1411260.1411266","type":"proceedings-article","created":{"date-parts":[[2008,9,23]],"date-time":"2008-09-23T13:39:01Z","timestamp":1222177141000},"page":"31-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["SASyLF"],"prefix":"10.1145","author":[{"given":"Jonathan","family":"Aldrich","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert J.","family":"Simmons","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Key","family":"Shin","sequence":"additional","affiliation":[{"name":"Microsoft Corporation, Redmond, WA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2008,9,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Machine-Verifiable Proofs for Teaching Constructive Logic. In Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs (PTP'01)","author":"Abel Andreas","year":"2001"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_1_4_1","unstructured":"Ian Barland Matthias Felleisen Kathi Fisler Phokion Kolaitis and Moshe Y. Vardi. Integrating Logic into the Computer Science Curriculum. http:\/\/www.cs.utexas.edu\/\\verb1 1csed\/FM\/docs\/iticse--fislervardi.pdf 2000.  Ian Barland Matthias Felleisen Kathi Fisler Phokion Kolaitis and Moshe Y. Vardi. Integrating Logic into the Computer Science Curriculum. http:\/\/www.cs.utexas.edu\/\\verb1 1csed\/FM\/docs\/iticse--fislervardi.pdf 2000."},{"key":"e_1_3_2_1_5_1","first-page":"93","volume-title":"The Digital Phoenix: How Computers are Changing Philosophy","author":"Barwise Jon","year":"1998"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_7_1","volume-title":"ACL2 Workshop","author":"Eastlund Carl","year":"2007"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"e_1_3_2_1_9_1","first-page":"143","article-title":"Using Programs to Teach Logic to Computer Scientists","volume":"40","author":"Goldson D.","year":"1993","journal-title":"Notices of the American Mathematical Society"},{"key":"e_1_3_2_1_10_1","unstructured":"Robert Harper. Practical Foundations for Programming Languages. Available at http:\/\/www.cs.cmu.edu\/~rwh\/plbook\/book.pdf 2008.   Robert Harper. Practical Foundations for Programming Languages. Available at http:\/\/www.cs.cmu.edu\/~rwh\/plbook\/book.pdf 2008."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_12_1","volume-title":"Matthias Felleisen. A Visual Environment for Developing Context-Sensitive Term Rewriting Systems. In International Conference on Rewriting Techniques and Applications. Springer Verlag LNCS 3091","author":"Matthews Jacob","year":"2004"},{"key":"e_1_3_2_1_13_1","first-page":"2283","article-title":"A Proof Assistant For Higher-Order Logic","author":"Nipkow Tobias","year":"2002","journal-title":"Lecture Notes in Computer Science"},{"key":"e_1_3_2_1_14_1","volume-title":"Linkoping University","author":"Pettersson Mikael","year":"1995"},{"key":"e_1_3_2_1_15_1","volume-title":"Elsevier Science and MIT Press","author":"Pfenning Frank","year":"2001"},{"key":"e_1_3_2_1_16_1","unstructured":"Frank Pfenning. Computation and Deduction. Cambridge University Press. In preparation. Draft from April 1997 available electronically at http:\/\/www.cs.cmu.edu\/~twelf\/notes\/cd.ps.  Frank Pfenning. Computation and Deduction. Cambridge University Press. In preparation. Draft from April 1997 available electronically at http:\/\/www.cs.cmu.edu\/~twelf\/notes\/cd.ps."},{"key":"e_1_3_2_1_17_1","first-page":"202","volume-title":"Pfenning and Carsten Sch\u00fcrmann. System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In International Conference on Automated Deduction","author":"Frank","year":"1999"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1080\/1049482940040203"},{"key":"e_1_3_2_1_19_1","volume-title":"Carnegie Mellon University","author":"Sch\u00fcrmann Carsten","year":"2000"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291155"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-5097-z"},{"key":"e_1_3_2_1_22_1","volume-title":"Research Corporation","author":"Tobias S.","year":"1992"},{"key":"e_1_3_2_1_23_1","unstructured":"Masaru Tomita. An Efficient Augmented-Context-Free Parsing Algorithm. phComputational Linguistics 13 (1-2): 31--46 1987.   Masaru Tomita. An Efficient Augmented-Context-Free Parsing Algorithm. phComputational Linguistics 13 (1-2): 31--46 1987."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/567097.567099"}],"event":{"name":"ICFP08: ACM SIGPLAN International Conference on Functional Programming","location":"Victoria BC Canada","acronym":"ICFP08","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 2008 international workshop on Functional and declarative programming in education"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1411260.1411266","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1411260.1411266","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:47Z","timestamp":1750253387000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1411260.1411266"}},"subtitle":["an educational proof assistant for language theory"],"short-title":[],"issued":{"date-parts":[[2008,9,21]]},"references-count":24,"alternative-id":["10.1145\/1411260.1411266","10.1145\/1411260"],"URL":"https:\/\/doi.org\/10.1145\/1411260.1411266","relation":{},"subject":[],"published":{"date-parts":[[2008,9,21]]},"assertion":[{"value":"2008-09-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}