{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:58Z","timestamp":1779836758932,"version":"3.53.1"},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2007,11,1]],"date-time":"2007-11-01T00:00:00Z","timestamp":1193875200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2007,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Design and quality are fundamental themes in engineering education. Functional programming builds software from small components, a central element of good design, and facilitates reasoning about correctness, an important aspect of quality. Software engineering courses that employ functional programming provide a platform for educating students in the design of quality software. This pearl describes experiments in the use of ACL2, a purely functional subset of Common Lisp with an embedded mechanical logic, to focus on design and correctness in software engineering courses. Students find the courses challenging and interesting. A few acquire enough skill to use an automated theorem prover on the job without additional training. Many students, but not quite a majority, find enough success to suggest that additional experience would make them effective users of mechanized logic in commercial software development. Nearly all gain a new perspective on what it means for software to be correct and acquire a good understanding of functional programming.<\/jats:p>","DOI":"10.1017\/s095679680700634x","type":"journal-article","created":{"date-parts":[[2007,4,26]],"date-time":"2007-04-26T04:36:24Z","timestamp":1177562184000},"page":"675-686","source":"Crossref","is-referenced-by-count":10,"title":["Engineering Software Correctness"],"prefix":"10.1017","volume":"17","author":[{"given":"REX","family":"PAGE","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2007,11,1]]},"reference":[{"key":"S095679680700634X_ref17","doi-asserted-by":"crossref","unstructured":"Vaillancourt D. , Page R. & Felleisen M. (2006) ACL2 in DrScheme. Pages 107\u2013116 of. Manolios P. & Wilding M. (eds), Proc. 6th International Workshop on the ACL2 Theorem Prover and Its Applications, 15\u201316 August 2006, Seattle, Washington. Ruben Gamboa.","DOI":"10.1145\/1217975.1217999"},{"key":"S095679680700634X_ref15","volume-title":"Software Engineering: A Practitioner's Approach","author":"Pressman","year":"2005"},{"key":"S095679680700634X_ref14","volume-title":"Proc. 2005 Workshop on Functional and Declarative Programming in Education, 25 September 2005, Tallinn, Estonia","author":"Page","year":"2005"},{"key":"S095679680700634X_ref13","doi-asserted-by":"crossref","unstructured":"Michaelsen L. K. (2002) Getting started with team based learning. Pages 27\u201329 of. Michaelsen L. K. Knight A. B. & Fink L. D. (eds), Team-Based Learning: A Transformative Use of Small Groups, Westport, CT: Praeger.","DOI":"10.4324\/9781003447535-3"},{"key":"S095679680700634X_ref5","doi-asserted-by":"crossref","unstructured":"Dillinger P. C. Manolios P. , Moore J. S. & Vroon D. (2006) ACL2s: the ACL2 Sedan. User Interfaces for Theorem Provers Workshop, August 2006, Seattle, WA. To appear in: Electronic Notes in Theoretical Computer Science. Available at: http:\/\/www.cc.gatech.edu\/~manolios\/research\/uitp-acl2s.html","DOI":"10.1016\/j.entcs.2006.09.018"},{"key":"S095679680700634X_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359106"},{"key":"S095679680700634X_ref3","volume-title":"Proc. 5th ACM SIGPLAN International Conference on Functional Programming","author":"Claessen","year":"2000"},{"key":"S095679680700634X_ref2","volume-title":"A Computational Logic Handbook","author":"Boyer","year":"1998"},{"key":"S095679680700634X_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004208"},{"key":"S095679680700634X_ref10","volume-title":"Software Abstractions: Logic, Language and Analysis","author":"Jackson","year":"2006"},{"key":"S095679680700634X_ref12","volume-title":"Computer Aided Reasoning: ACL2 Case Sudies","author":"Kaufmann","year":"2000"},{"key":"S095679680700634X_ref8","unstructured":"Humphrey W. S. (1995) A Discipline for Software Engineering. Addison Wesley."},{"key":"S095679680700634X_ref7","volume-title":"Pages of 48\u201359 of. Proc. 7th ACM SIGPLAN International Conference on Functional Programming","author":"Findler","year":"2002"},{"key":"S095679680700634X_ref11","volume-title":"Computer Aided Reasoning: An Approach","author":"Kaufmann","year":"2000"},{"key":"S095679680700634X_ref1","unstructured":"Bjorner D. (2006) Software Engineering 1: Abstraction and Modelling. Springer."},{"key":"S095679680700634X_ref16","doi-asserted-by":"crossref","unstructured":"Sommerville I. (2004) Software Engineering, 7th ed. Pearson.","DOI":"10.1049\/ic:20040184"},{"key":"S095679680700634X_ref9","unstructured":"IEEE Computer Society\/ACM Joint Task Force on Computing Curricula. (2004) Software Engineering 2004: Curriculum Guidelines for Undergraduate Degree Programs in Software Engineering. Available at: http:\/\/sites.computer.org\/ccse\/SE2004Volume.pdf"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679680700634X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:37:03Z","timestamp":1779835023000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679680700634X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11]]},"references-count":17,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2007,11]]}},"alternative-id":["S095679680700634X"],"URL":"https:\/\/doi.org\/10.1017\/s095679680700634x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,11]]}}}