pith. sign in

arxiv: 1907.04134 · v1 · pith:5OM4ZMP2new · submitted 2019-07-07 · 💻 cs.PL · cs.LO

A Bridge Anchored on Both Sides: Formal Deduction in Introductory CS, and Code Proofs in Discrete Math

David G. Wonnacott , Peter-Michael Osera This is my paper

Pith reviewed 2026-05-25 01:10 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords formal deductionCS1discrete mathematicscode reasoningsymbolic executionproof assistantcurriculum integrationundergraduate education
0
0 comments X

The pith

Formal reasoning about programs bridges CS1 and introductory discrete mathematics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper aims to show that formal reasoning about programs serves as an effective bridge between introductory programming in CS1 and discrete mathematics. By adapting symbolic execution techniques for code reasoning in both courses, the disconnect between coding and math can be reduced for students. Haverford College integrates this in its CS1 with a 3-2-1 curriculum, and Grinnell College uses it to motivate logic in discrete math. The authors also introduce Orca as a proof assistant to improve feedback on student proofs. This leads to open research questions on the approach's effectiveness for wider use.

Core claim

The authors establish that code reasoning, presented via symbolic execution style tuned to each course, anchors formal deduction in CS1 at Haverford and code proofs in discrete math at Grinnell, creating a bridge across the curriculum. This uses traditional pen-and-paper initially but moves toward tool support with Orca to handle feedback issues, while identifying next steps for educational research.

What carries the argument

The bridge of formal reasoning about programs using a style based on symbolic code execution techniques from the programming language community.

If this is right

  • Students gain better understanding of the relationship between programs and mathematical reasoning.
  • Instructors at typical institutions can incorporate this without major course overhauls.
  • Proof assistants like Orca can reduce the grading burden and provide timely feedback.
  • The experiences raise concrete research questions that can guide further studies and generalization.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Adapting the approach more widely could help address the common curriculum disconnect in CS programs.
  • Development of tools like Orca may enable scalable support for proof-based pedagogy.
  • The posed research questions suggest opportunities to measure impacts on student learning outcomes.

Load-bearing premise

The style of code reasoning based on symbolic execution techniques can be adapted to the constraints of both CS1 and discrete math courses without requiring substantial additional instructor training or changes to existing course structures.

What would settle it

A controlled comparison of student understanding of the link between programming and mathematics in bridged versus traditional courses, or reports from instructors on the training required to implement the approach.

Figures

Figures reproduced from arXiv: 1907.04134 by David G. Wonnacott, Peter-Michael Osera.

Figure 1
Figure 1. Figure 1: Code for an early example of execution [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Executing figure 1 in the Idle debugger. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Executing figure 1 in Orca. x name-to-def (x) 2*a+2*b name-to-def (a) 2*14+2*b name-to-def (b) 2*14+2*7 arithmetic 42 [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Complete substitution sequence for figure 1 [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Substituting a definition later for figure 1. [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Recommending punctuation, statement form. [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Recommending punctuation, expression form. [PITH_FULL_IMAGE:figures/full_fig_p008_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Function calls, conditionals, strings. substituting-away all local variables with the name-to-def rule, and converting if’s to expression form (as discussed in Section 2.2). As with the name-to-def rule, we can only apply this rule if the expressions used to define local variables, and the expressions for argList, are safe [PITH_FULL_IMAGE:figures/full_fig_p009_8.png] view at source ↗
Figure 6
Figure 6. Figure 6: The sequence for the code of Figure 7 would be identical, except for the factoring-out of the [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
Figure 9
Figure 9. Figure 9: Function definition rules. import math a=5 b=2 # |- # add 17 to a to the b'th power 17+math.pow(a, b) [PITH_FULL_IMAGE:figures/full_fig_p010_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Code that calls a library function. 17+math.pow(a, b) name-to-def (a and b) 17+math.pow(5, 2) name-to-spec (math.pow) 17+5 2 arithmetic 42.0 [PITH_FULL_IMAGE:figures/full_fig_p010_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Executing the code of figure 10. As in other situations, the order of substitutions for [PITH_FULL_IMAGE:figures/full_fig_p010_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Substituting variables late for figure 10. [PITH_FULL_IMAGE:figures/full_fig_p011_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Recursive power function, call thereof. power(x, y) name-to-def (x and y) power(3+2, 2) arithmetic power(5, 2) name-to-body ( 5 if 2 == 1 else 5 * power(x, 2-1) ) arithmetic ( 5 if False else 5 * power(5, 1) ) if-False 5 * power(5, 1) name-to-body 5 * ( 5 if 1 == 1 else 5 * power(x, 1-1) ) arithmetic 5 * ( 5 if True else 5 * power(5, 1-1) ) if-True 5 * ( 5 ) arithmetic 25 [PITH_FULL_IMAGE:figures/full_fi… view at source ↗
Figure 14
Figure 14. Figure 14: Executing a recursive function. Note that [PITH_FULL_IMAGE:figures/full_fig_p012_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Executing power(x, 2) without a value for x. result, i.e., power(b, e) should return b**e, and argList is legal, i.e., e>0. However, we are not allowed to apply the rule, since power is not (yet) a trusted function. To complete the sequence of substitutions from power(x, y) to x**y, we’ll need to introduce our third (and final) function-call rule. This rule lets a recursive function trust itself during th… view at source ↗
Figure 16
Figure 16. Figure 16: Verifying correctness of power [PITH_FULL_IMAGE:figures/full_fig_p018_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Example Coq proof state. • intros l1 l2 introduces the universally quantified variables l1 and l2 into the proof as unknown values. • induction l1 performs induction over l1. • simpl tells Coq to simplify the goal, equivalent to the −→∗ stepping relation we used in the paper proof. • rewrite IHl1 rewrites the goal according to our induction hypothesis. • reflexivity discharges the proof obligation if the … view at source ↗
Figure 18
Figure 18. Figure 18: Example even logic declared in Orca [PITH_FULL_IMAGE:figures/full_fig_p027_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: Context lookup action in Orca. relation, EvenRel, with a sole constructor that takes a Nat as an argument. The eDSL uses Haskell’s generic deriving mechanism to automatically tie these datatypes to Core Orca’s internal representations for symbols and relations. All subsequent definitions use these datatypes and Haskell’s type system ensures that we do not mix up sorts and relations in erroneous ways. We d… view at source ↗
Figure 20
Figure 20. Figure 20: Inference rule declaration of if-True in Orca. equivalent to the final version of the rule as realized in Orca: if-true-orca e = E[e1 if True else e2] e ′ = E[e1] e −→ e ′ 5.2.5 Block-based Front-end. To ease adoption in undergraduate classrooms, Orca is a web application immediately accessible to undergraduates through any modern web browser. The back-end server application is customized by the instructo… view at source ↗
Figure 21
Figure 21. Figure 21: even(4) as realized in Orca 6 INTEGRATING CS1 AND DM The CS1 and Discrete Mathematics curricula described above do not currently exist in the same environment; Haverford’s CS1 is paired with a discrete math course that does not feature Orca (or Coq), and Grinnell’s discrete math is paired with a CS introductory course without explicit code reasoning. The relationships between proof-construction, reasoning… view at source ↗
read the original abstract

There is a sharp disconnect between the programming and mathematical portions of the standard undergraduate computer science curriculum, leading to student misunderstanding about how the two are related. We propose connecting the subjects early in the curriculum---specifically, in CS1 and the introductory discrete mathematics course---by using formal reasoning about programs as a bridge between them. This article reports on Haverford and Grinnell College's experience in constructing the end points of this bridge between CS1 and discrete mathematics. Haverford's long-standing "3-2-1" curriculum introduces code reasoning in conjunction with introductory programming concepts, and Grinnell's discrete mathematics introduces code reasoning as a motivation for logic and formal deduction. Both courses present code reasoning in a style based on symbolic code execution techniques from the programming language community, but tuned to address the particulars of each course. These courses rely primarily on traditional means of proof authoring with pen-and-paper. This is unsatisfactory for students who receive no feedback until grading on their work and instructors who must shoulder the burden of interpreting students' proofs and giving useful feedback. To this end, we also describe the current state of Orca, an in-development proof assistant for undergraduate education that we are developing to address these issues in our courses. Finally, in teaching our courses, we have discovered a number of educational research questions about the effectiveness of code reasoning in bridging the gap between programming and mathematics, and the ability of tools like \orca to support this pedagogy. We pose these research questions as next steps to formalize our initial experiences in our courses with the hope of eventually generalizing our approaches for wider adoption.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper proposes using formal reasoning about programs (based on symbolic execution techniques) as a bridge to connect the programming and mathematical components of the undergraduate CS curriculum, specifically in CS1 and introductory discrete mathematics. It reports on experiences implementing this at Haverford College (via its 3-2-1 curriculum) and Grinnell College (via its discrete math course), describes the in-development Orca proof assistant for pen-and-paper style proofs, and poses open educational research questions about effectiveness and tool support.

Significance. If the approach can be validated, it offers a practical way to address a longstanding curricular disconnect in CS education by integrating formal methods early. The specific course adaptations at two institutions and the description of Orca provide concrete examples that could inform similar efforts elsewhere, while the research questions usefully identify directions for empirical work. The manuscript correctly frames itself as an experience report rather than a validated outcome study.

minor comments (2)
  1. The abstract and text refer to the tool as both 'Orca' and 'orca' (with LaTeX macro); standardize capitalization and formatting for consistency.
  2. The description of Orca's current state is high-level; adding a short paragraph on its implemented features versus planned ones would improve clarity for readers interested in adoption.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the thoughtful and positive review, including the recognition that the work is appropriately framed as an experience report. We are pleased that the referee sees value in the curricular bridge concept, the concrete examples from Haverford and Grinnell, and the open research questions posed.

Circularity Check

0 steps flagged

No circularity: purely descriptive experience report

full rationale

The manuscript is an experience report on course practices at Haverford and Grinnell plus open research questions. It contains no equations, derivations, fitted parameters, predictions, or load-bearing self-citations. All claims reduce to direct description of what was implemented at the two institutions, with no reduction of any result to its own inputs by construction. The central proposal is framed as a suggestion supported by local experience rather than a theorem or generalization proven within the paper.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper contains no mathematical derivations, empirical models, or technical claims that introduce free parameters, axioms, or invented entities; it is an educational proposal and experience report.

pith-pipeline@v0.9.0 · 5835 in / 1072 out tokens · 21103 ms · 2026-05-25T01:10:14.314801+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

40 extracted references · 40 canonical work pages

  1. [1]

    Structure and interpretation of computer programs

    Harold Abelson, Gerald Jay Sussman, and Julie Sussman. Structure and interpretation of computer programs . Justin Kelly, 1996

    work page 1996

  2. [2]

    Characterizing Students’ Difficulty with Proof by Mathematical Induction

    John Douglas Baker. Characterizing Students’ Difficulty with Proof by Mathematical Induction. PhD thesis, Indiana University, 1995

    work page 1995

  3. [3]

    Orc2a: A proof assistant for undergraduate education

    Jianting Chen, Medha Gopalaswamy, Prabir Pradhan, Sooji Son, and Peter-Michael Osera. Orc2a: A proof assistant for undergraduate education. In Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education , SIGCSE ’17, pages 757–758, New York, NY, USA, 2017. ACM. ISBN 978-1-4503-4698-6. doi: 10.1145/3017680.3022466. URL http://doi.a...

    work page doi:10.1145/3017680.3022466 2017

  4. [4]

    The calculus of constructions

    Thierry Coquand and Gerard Huet. The calculus of constructions. Inf. Comput., 76(2-3):95–120, February 1988. ISSN 0890-5401. doi: 10.1016/ 0890-5401(88)90005-3. URL http://dx.doi.org/10.1016/0890-5401(88)90005-3

    work page doi:10.1016/0890-5401(88)90005-3 1988

  5. [5]

    The Coq proof assistant reference manual

    The Coq development team. The Coq proof assistant reference manual . LogiCal Project, 2004. URL http://coq.inria.fr. Version 8.0; see http://coq.inria.fr

    work page 2004

  6. [6]

    Dougherty and David G

    John P. Dougherty and David G. Wonnacott. Use and assessment of a rigorous approach to cs1. InProceedings of the 36th SIGCSE Technical Symposium on Computer Science Education , SIGCSE ’05, pages 251–255, New York, NY, USA, 2005. ACM. ISBN 1-58113-997-7. doi: 10.1145/1047344.1047431. URL http://doi.acm.org/10.1145/1047344.1047431

    work page doi:10.1145/1047344.1047431 2005

  7. [7]

    The black box inside the glass box

    BENEDICT DU BOULAY, TIM O’SHEA, and JOHN MONK. The black box inside the glass box. Int. J. Hum.-Comput. Stud. , 51(2):265–277, August

    work page

  8. [8]

    doi: 10.1006/ijhc.1981.0309

    ISSN 1071-5819. doi: 10.1006/ijhc.1981.0309. URL http://dx.doi.org/10.1006/ijhc.1981.0309

    work page doi:10.1006/ijhc.1981.0309 1981

  9. [9]

    Teaching mathematical induction i

    Ed Dubinsky. Teaching mathematical induction i. Journal of Mathematical Behavior , 5:305–317, 1986

    work page 1986

  10. [10]

    Teaching mathematical induction ii

    Ed Dubinsky. Teaching mathematical induction ii. Journal of Mathematical Behavior , 8:285–304, 1989

    work page 1989

  11. [11]

    Exploring experienced professionals’ reflections on computing education

    Marisa Exter and Nichole Turnage. Exploring experienced professionals’ reflections on computing education. Trans. Comput. Educ., 12(3): 12:1–12:23, July 2012. ISSN 1946-6226. doi: 10.1145/2275597.2275601. URL http://doi.acm.org/10.1145/2275597.2275601

    work page doi:10.1145/2275597.2275601 2012

  12. [12]

    The revised report on the syntactic theories of sequential control and state

    Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103(2):235–271, September 1992. ISSN 0304-3975. doi: 10.1016/0304-3975(92)90014-7. URL http://dx.doi.org/10.1016/0304-3975(92)90014-7

    work page doi:10.1016/0304-3975(92)90014-7 1992

  13. [13]

    How to design programs: an introduction to programming and computing

    Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. How to design programs: an introduction to programming and computing. MIT Press, 2018. A Bridge Anchored on Both Sides 35

    work page 2018

  14. [14]

    Assessing and teaching scope, mutation, and aliasing in upper-level undergraduates

    Kathi Fisler, Shriram Krishnamurthi, and Preston Tunnell Wilson. Assessing and teaching scope, mutation, and aliasing in upper-level undergraduates. In Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education , SIGCSE ’17, pages 213–218, New York, NY, USA, 2017. ACM. ISBN 978-1-4503-4698-6. doi: 10.1145/3017680.3017777. URL htt...

    work page doi:10.1145/3017680.3017777 2017

  15. [15]

    The four colour theorem: Engineering of a formal proof

    Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Deepak Kapur, editor,Computer Mathematics, pages 333–333. Springer- Verlag, Berlin, Heidelberg, 2008. ISBN 978-3-540-87826-1. doi: 10.1007/978-3-540-87827-8_28. URL http://dx.doi.org/10.1007/978-3-540-87827-8_28

    work page doi:10.1007/978-3-540-87827-8_28 2008

  16. [16]

    A machine-checked proof of the odd order theorem

    Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Proceedings of the 4th International Conference on Interactive...

    work page doi:10.1007/978-3-642-39634-2_14 2013

  17. [17]

    The Certificate in Education and Training

    Ann Gravells and Susan Simpson. The Certificate in Education and Training . Sage Publishing Company, 2014. ISBN 1446295885

    work page 2014

  18. [18]

    Michael Greenberg and Joseph C. Osborn. Teaching discrete mathematics to early undergraduates with software foundations. In CoqPL 2019, 2019

    work page 2019

  19. [19]

    A formal proof of the kepler conjecture

    THOMAS HALES, MARK ADAMS, GERTRUD BAUER, TAT DAT DANG, JOHN HARRISON, LE TRUONG HOANG, CEZARY KALISZYK, VICTOR MAGRON, SEAN MCLAUGHLIN, TATÂăTHANG NGUYEN, and et al. A formal proof of the kepler conjecture. Forum of Mathematics, Pi , 5:e2, 2017. doi: 10.1017/fmp.2017.1

    work page doi:10.1017/fmp.2017.1 2017

  20. [20]

    Hacker-proof code confirmed

    Kevin Hartnett. Hacker-proof code confirmed. Quanta Magazine , September 2016. URL https://www.quantamagazine.org/ 20160920-formal-verification-creates-hacker-proof-code/

    work page 2016

  21. [21]

    Andrew J. Haven. Automated proof checking in introductory discrete mathematics classes. Master’s thesis, Massachusetts Institute of Technology, 2012

    work page 2012

  22. [22]

    Computer Science Curricula 2013: Curriculum Guidelines for Undergraduate Degree Programs in Computer Science

    Association for Computing Machinery (ACM) Joint Task Force on Computing Curricula and IEEE Computer Society. Computer Science Curricula 2013: Curriculum Guidelines for Undergraduate Degree Programs in Computer Science . ACM, New York, NY, USA, 2013. ISBN 978-1-4503-2309-3. 999133

    work page 2013

  23. [23]

    Communications of the ACM 52(7), pp

    Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107–115, July 2009. ISSN 0001-0782. doi: 10.1145/1538788.1538814. URL http://doi.acm.org/10.1145/1538788.1538814

    work page doi:10.1145/1538788.1538814 2009

  24. [24]

    Program development in JA V A: abstraction, specification, and object-oriented design

    Barbara Liskov and John Guttag. Program development in JA V A: abstraction, specification, and object-oriented design. Pearson Education, 2000

    work page 2000

  25. [25]

    Abstraction and specification in program development , volume 180

    Barbara Liskov, John Guttag, et al. Abstraction and specification in program development , volume 180. MIT press Cambridge, 1986

    work page 1986

  26. [26]

    Introduction to Algorithms: A Creative Approach

    Udi Manber. Introduction to Algorithms: A Creative Approach . Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1989. ISBN 0201120372

    work page 1989

  27. [27]

    A blocks-based language for program correctness proofs

    Peter-Michael Osera and David Wonnacott. A blocks-based language for program correctness proofs. In 2017 IEEE Blocks and Beyond Workshop (B&B), October 2017

    work page 2017

  28. [28]

    Making induction meaningful, recursively (abstract only)

    Peter-Michael Osera and Brent Yorgey. Making induction meaningful, recursively (abstract only). InProceedings of the 45th ACM Technical Symposium on Computer Science Education , SIGCSE ’14, pages 737–737, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2605-6. doi: 10.1145/2538862.2544262. URL http://doi.acm.org/10.1145/2538862.2544262

    work page doi:10.1145/2538862.2544262 2014

  29. [29]

    Pasternak, R

    E. Pasternak, R. Fenichel, and A. N. Marshall. Tips for creating a block language with blockly. In 2017 IEEE Blocks and Beyond Workshop (B B) , pages 21–24, Oct 2017. doi: 10.1109/BLOCKS.2017.8120404

    work page doi:10.1109/blocks.2017.8120404 2017

  30. [30]

    Benjamin C. Pierce. Lambda, the ultimate ta: Using a proof assistant to teach programming language foundations. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming , ICFP ’09, pages 121–122, New York, NY, USA, 2009. ACM. ISBN 978-1-60558-332-7. doi: 10.1145/1596550.1596552. URL http://doi.acm.org/10.1145/1596550.1596552

    work page doi:10.1145/1596550.1596552 2009

  31. [31]

    Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hriţcu, Vilhelm Sjoberg, and Brent Yorgey.Software Foundations

    Benjamin C. Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hriţcu, Vilhelm Sjoberg, and Brent Yorgey.Software Foundations. Electronic textbook, 2015

    work page 2015

  32. [32]

    Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey

    Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations. Software Foundations series, volume 2. Electronic textbook, May 2018

    work page 2018

  33. [33]

    Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey

    Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. Logical Foundations. Software Foundations series, volume 1. Electronic textbook, May 2018

    work page 2018

  34. [34]

    A conceptual approach to teaching induction for computer science

    Irene Polycarpou, Ana Pasztor, and Malek Adjouadi. A conceptual approach to teaching induction for computer science. In Proceedings of the 39th SIGCSE Technical Symposium on Computer Science Education , SIGCSE ’08, pages 9–13, New York, NY, USA, 2008. ACM. ISBN 978-1-59593-799-5. doi: 10.1145/1352135.1352142. URL http://doi.acm.org/10.1145/1352135.1352142

    work page doi:10.1145/1352135.1352142 2008

  35. [35]

    Logic and Proofs

    Richard Scheines and Wilfried Sieg. Computer environments for proof construction. Interactive Learning Environments, 4(2):159–169, 1994. doi: 10.1080/1049482940040203. URL http://dx.doi.org/10.1080/1049482940040203. See also the online course “Logic and Proofs” at Carnegie Mellon University

    work page doi:10.1080/1049482940040203 1994

  36. [36]

    Notional machines and introductory programming education

    Juha Sorva. Notional machines and introductory programming education. Trans. Comput. Educ., 13(2):8:1–8:31, July 2013. ISSN 1946-6226. doi: 10.1145/2483710.2483713. URL http://doi.acm.org/10.1145/2483710.2483713

    work page doi:10.1145/2483710.2483713 2013

  37. [37]

    In: Proceedings of the 49th ACM Technical Symposium on Computer Science Education, SIGCSE ’18, ACM, pp

    Preston Tunnell Wilson, Kathi Fisler, and Shriram Krishnamurthi. Evaluating the tracing of recursion in the substitution notional machine. In Proceedings of the 49th ACM Technical Symposium on Computer Science Education , SIGCSE ’18, pages 1023–1028, New York, NY, USA, 2018. ACM. ISBN 978-1-4503-5103-4. doi: 10.1145/3159450.3159479. URL http://doi.acm.org...

    work page doi:10.1145/3159450.3159479 2018

  38. [38]

    A. M. Turing. Computability and Îż-definability. Journal of Symbolic Logic , 2(4):153âĂŞ163, 1937. doi: 10.2307/2268280

    work page doi:10.2307/2268280 1937

  39. [39]

    Velleman

    Daniel J. Velleman. How to prove it: a structured approach . Cambridge University Press, 2006. 36 David G. Wonnacott and Peter-Michael Osera

    work page 2006

  40. [40]

    From Vision to Execution: The Creative Process in Computer Science

    David Wonnacott. From Vision to Execution: The Creative Process in Computer Science . lulu.com, Raleigh, North Carolina, USA, 2017. Lulu.com ID 1094615. See http://cs.haverford.edu/faculty/davew/FVtE/FVtE-current.pdf, or, for Fall 2017 edition, http://cs.haverford.edu/faculty/davew/FVtE/FVtE-2017.pdf

    work page 2017