research-article

Functional programming and theorem proving for undergraduates: a progress report

Authors:

Matthias FelleisenAuthors Info & Claims

FDPE '08: Proceedings of the 2008 international workshop on Functional and declarative programming in education

Pages 21 - 30

https://doi.org/10.1145/1411260.1411264

Published: 21 September 2008 Publication History

Abstract

For the past five years, the University of Oklahoma has used the ACL2 theorem prover for a year-long sequence on software engineering. The goal of the course is to introduce students to functional programming with "Applicative Common Lisp" (ACL) and to expose them to defect recognition at all levels, including unit testing, randomized testing of conjectures, and formal theorem proving in "a Computational Logic" (ACL2).

Following Page's example, Northeastern University has experimented with the introduction of ACL2 into the freshman curriculum for the past two years. Northeastern's goal is to supplement an introductory course on functional program design with a course on logic and theorem proving that integrates the topic with programming projects.

This paper reports on our joint project's progress. On the technical side, the paper presents the Scheme-based integrated development environment, its run-time environment for functional GUI programming, and its support for different forms of testing. On the experience side, the paper summarizes the introduction of these tools into the courses, the reaction of industrial observers of Oklahoma's software engineering course, and the feedback from a first outreach workshop.

References

[1]

Achten, P. and M. J. Plasmeijer. The ins and outs of Clean i/o. Journal of Functional Programming, 5(1):81--110, 1995.

[2]

Arts, T. and J. Hughes. Erlang/QuickCheck. In Ninth International Erlang/OTP User Conference, November 2003.

[3]

Beck, K. and E. Gamma. Test infected: Programmers love writing tests. In Java Report, volume 3, pages 37--50, 1998.

[4]

Boyer, R. S. and J. S. Moore. Mechanized reasoning about programs and computing machines. In Veroff, R., editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pages 146--176. The MIT Press, Cambridge, Massachusetts, 1996.

Digital Library

[5]

Claessen, K. and J. Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. In ACM SIGPLAN International Conference on Functional Programming, pages 268--279, 2000.

Digital Library

[6]

Cooper, G. H. and S. Krishnamurthi. Embedding dynamic dataflow in a call-by-value language. In Sestoft, P., editor, 15th European Symposium on Programming, ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 294--308. Springer, 2006.

Digital Library

[7]

Dillinger, P. C., P. Manolios, J. S. Moore and D. Vroon. ACL2s: The ACL2 Sedan. In Proceedings of the 7th Workshop on User Interfaces for Theorem Proving, volume 174(2) of Electronic Notes in Theoretical Computer Science, pages 3--18. Elsevier, 2006.

Digital Library

[8]

Eastlund, C., D. Vaillancourt and M. Felleisen. ACL2 for freshmen: First experiences. In ACL2 '07: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, pages 200--211, New York, NY, USA, 2007. ACM Press.

[9]

Elliot, C. and P. Hudak. Functional reactive animation. In ACM SIGPLAN International Conference on Functional Programming, pages 196--203, 1997.

Digital Library

[10]

Felleisen, M., R. B. Findler, M. Flatt and S. Krishnamurthi. How to Design Programs. MIT Press, 2001.

[11]

Findler, R. B., J. Clements, C. Flanagan, M. Flatt, S. Krishnamurthi, P. Steckler and M. Felleisen. DrScheme: A programming environment for Scheme. Journal of Functional Programming, 12(2):159--182, March 2002.

Digital Library

[12]

Findler, R. B., C. Flanagan, M. Flatt, S. Krishnamurthi and M. Felleisen. DrScheme: A pedagogic programming environment for Scheme. In Glaser, H., P. Hartel and H. Kuchen, editors, Programming Languages: Implementations, Logics, and Programs, volume 1292 of LNCS, pages 369--388, Southampton, UK, September 1997. Springer.

Digital Library

[13]

Ignatoff, D., G. H. Cooper and S. Krishnamurthi. Crossing state lines: Adapting object-oriented frameworks to functional reactive languages. In Hagiya, M. and P. Wadler, editors, Functional and Logic Programming, 8th International Symposium, FLOPS 2006, volume 3945 of Lecture Notes in Computer Science, pages 259--276. Springer, 2006.

[14]

Kaufmann, M., P. Manolios and J. S. Moore. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, 2000.

Digital Library

[15]

Kaufmann, M., P. Manolios and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.

Digital Library

[16]

Page, R. Software is discrete mathematics. In Runciman, C. and O. Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, pages 79--86. ACM, August 2003.

Digital Library

[17]

Page, R. Engineering software correctness. In Proc. 2005 Workshop on Functional and Declarative Programming in Education, pages 39--46, New York, NY, USA, 2005. ACM.

Digital Library

[18]

Page, R. Engineering software correctness. Journal of Functional Programming, 17(6):675--686, April 2007. Preliminary presentation at FDPE '05.

Digital Library

[19]

Vaillancourt, D., R. Page and M. Felleisen. ACL2 in DrScheme. In ACL2 '06: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, pages 107--116, New York, NY, USA, 2006. ACM Press.

Digital Library

Cited By

Gamboa RThoney A(2022)Using ACL2 To Teach Students About Software TestingElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.359.4359(19-32)Online publication date: 24-May-2022
https://doi.org/10.4204/EPTCS.359.4
Schoolderman MSmetsers Svan Eekelen M(2019)Is Deductive Program Verification Mature Enough to be Taught to Software Engineers?Proceedings of the 8th Computer Science Education Research Conference10.1145/3375258.3375265(50-57)Online publication date: 18-Nov-2019
https://dl.acm.org/doi/10.1145/3375258.3375265
Page RGamboa R(2013)How Computers Work: Computational Thinking for EveryoneElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.106.1106(1-19)Online publication date: 20-Jan-2013
https://doi.org/10.4204/EPTCS.106.1
Show More Cited By

Index Terms

Recommendations

Theorem Proving Modulo
Abstract
Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...
Proof-checking metamathematics (theorem-proving)
Theorem proving and programming with dynamic first order logic

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FDPE '08: Proceedings of the 2008 international workshop on Functional and declarative programming in education

September 2008

98 pages

ISBN:9781605580685

DOI:10.1145/1411260

Program Chairs:
Frank Huch
University of Kiel, Germany
,
Adam Parkin
University of Victory, Canada

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 September 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP08

Sponsor:

ICFP08: ACM SIGPLAN International Conference on Functional Programming

September 21, 2008

BC, Victoria, Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
344
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gamboa RThoney A(2022)Using ACL2 To Teach Students About Software TestingElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.359.4359(19-32)Online publication date: 24-May-2022
https://doi.org/10.4204/EPTCS.359.4
Schoolderman MSmetsers Svan Eekelen M(2019)Is Deductive Program Verification Mature Enough to be Taught to Software Engineers?Proceedings of the 8th Computer Science Education Research Conference10.1145/3375258.3375265(50-57)Online publication date: 18-Nov-2019
https://dl.acm.org/doi/10.1145/3375258.3375265
Page RGamboa R(2013)How Computers Work: Computational Thinking for EveryoneElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.106.1106(1-19)Online publication date: 20-Jan-2013
https://doi.org/10.4204/EPTCS.106.1
St-Amour VToronto N(2013)Experience reportACM SIGPLAN Notices10.1145/2544174.250061648:9(351-356)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2544174.2500616
St-Amour VToronto NMorrisett GUustalu T(2013)Experience reportProceedings of the 18th ACM SIGPLAN international conference on Functional programming10.1145/2500365.2500616(351-356)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2500365.2500616
Rößling G(2012)A Family of Tools for Supporting the Learning of ProgrammingComputer Technology and Computer Programming10.1201/b13124-11(213-230)Online publication date: 17-Oct-2012
https://doi.org/10.1201/b13124-11
Nipkow T(2012)Teaching semantics with a proof assistantProceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation10.1007/978-3-642-27940-9_3(24-38)Online publication date: 22-Jan-2012
https://dl.acm.org/doi/10.1007/978-3-642-27940-9_3
Rößling G(2010)A Family of Tools for Supporting the Learning of ProgrammingAlgorithms10.3390/a30201683:2(168-182)Online publication date: 15-Apr-2010
https://doi.org/10.3390/a3020168
Felleisen M(2010)TeachScheme!ACM SIGPLAN Notices10.1145/1932681.186356345:9(129-130)Online publication date: 27-Sep-2010
https://dl.acm.org/doi/10.1145/1932681.1863563
Felleisen MHudak PWeirich S(2010)TeachScheme!Proceedings of the 15th ACM SIGPLAN international conference on Functional programming10.1145/1863543.1863563(129-130)Online publication date: 27-Sep-2010
https://dl.acm.org/doi/10.1145/1863543.1863563
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten