The software industry is clamoring for computer science undergraduates to know how to ''Use AI'' for software development. But it isn't clear what ''Using AI'' entails, especially as the technology rapidly evolves. While industry has created this narrative, it is educators that must drive it to its conclusion by identifying specific skills graduates need to effectively use present-day AI tools and foundational principles that will help graduates use them in the future. There are many ideas proposed about what the future of programming looks like, from prompt engineering to agentic/cybernetic programming, but little consensus as to what students ought to learn. Because the landscape is constantly evolving, continued discussion is necessary for educators to keep up or stay ahead of these changes.

Mathematics is often considered the foundation of computer science, with rigorous, mathematical reasoning, i.e., proof, at the heart of this foundation. Mathematical proof is the backbone of virtually all introductory mathematics courses within any computer science major. However, the degree to which rigorous reasoning is required of students in subsequent courses is highly variable across institutions. At some institutions, proof is a tool used to deepen material, whereas, at other places, proof is set aside in favor of increased topic coverage. Consequently, many students do not see the purpose of proof in computing. Furthermore, the demands of rigorous mathematical reasoning dissuade many students from continuing in the field.

Notional Machines (NMs) are a pedagogical device used by teachers in order to help students understand certain concepts. While NMs have been cataloged, the effectiveness of NMs has been rarely evaluated. We build upon this research by exploring what makes certain NMs more effective in various computer science and mathematics courses. We interview professors and students to assess NMs used in the classroom. Notably we found that most students are able to employ the NMs introduced by their professors, and that introductory students prefer template-like NMs, whereas upper level students rely on more conceptual NMs.

Chemical reaction networks (CRNs) are an important tool for molecular programming, a field that is rapidly expanding our ability to deploy computer programs into biological systems for a variety of applications. However, CRNs are also difficult to work with due to their massively parallel nature, leading to the need for higher-level languages that allow for easier computation with CRNs. Recently, research has been conducted into a variety of higher-level languages for deterministic CRNs but modeling CRN parallelism, managing error accumulation, and finding natural CRN representations are ongoing challenges. We introduce Reactamole, a higher-level language for deterministic CRNs that utilizes the functional reactive programming (FRP) paradigm to represent CRNs as a reactive dataflow network. Reactamole equates a CRN with a functional reactive program, implementing the key primitives of the FRP paradigm directly as CRNs. The functional nature of Reactamole makes reasoning about molecular programs easier, and its strong static typing allows us to ensure that a CRN is well-formed by virtue of being well-typed. In this paper, we describe the design of Reactamole and how we use CRNs to represent the common datatypes and operations found in FRP. We also demonstrate the potential of this functional reactive approach to molecular programming by giving an extended example where a CRN is constructed using FRP to modulate and demodulate an amplitude modulated signal.

Mathematics requirements for computer science students vary broadly by institution. The general question of what mathematics should be required of computer science majors naturally leads to more specific questions such as: What mathematics content should be required? What mathematical concepts? Should the theory of computation be required? Should calculus, discrete mathematics, probability, and/or linear algebra? What impact do newer fields such as data science and machine learning have on the mathematics needed or required for computer science majors? What are faculty members doing to integrate mathematics into their computer science courses and does this help some students overcome difficulties learning the mathematics? What level of mathematical maturity should a computer science graduate attain? In this session, participants will share their answers to these questions with the goal of coming to a broader understanding of how mathematics informs the discipline. Through this discussion, we will try to reconcile our idealized curriculum with the practical reality of requirements, dependencies, and limits imposed by our institutions.

Diagnostic messages generated by compilers and interpreters such as syntax error messages have been researched for decades. Unfortunately these messages which include error, warning, and runtime messages, present substantial difficulty and could be more effective, particularly for novices. Recent years have seen increased number of papers in the area including studies on the effectiveness of these messages, improving or enhancing them, and their usefulness as a part of programming process data that can be used to predict student performance. Despite this increased interest, the long history of literature is quite scattered and has not been brought together in any digestible form. We argue that in order to help the community proceed with more work on diagnostic messages, the literature needs to be presented in a state-of-the-art report. In addition we will synthesize and present the existing evidence for these messages including the difficulties they present and their effectiveness. We will also formulate a set of guidelines based on this evidence that can be used when designing or enhancing diagnostic messages. This work can serve as a starting point for those who wish to conduct research on such messages, those who wish to design better messages or those that aim to measure their effectiveness, more effectively.

The undergraduate computer science curriculum is ever-changing but has seen particular turmoil recently. Topics such as machine learning, data science, and concurrency and parallelism have grown in importance over the last few years. As the content of our curriculum changes, so too does the mathematical foundations on which it rests. Do our current theoretical courses adequately support these foundations or must we consider new pedagogy that is more relevant to our students' needs? In this BoF, we will discuss what a modern mathematics curriculum for computer scientists should cover and how we should go about accomplishing this in our classrooms.

There is a natural correspondence between mathematical proofs and computer programs. For instance, a recursive function and its correctness relate directly to inductive proofs in mathematics. However, many undergraduate students feel a disconnect between mathematics and computer science. There are several proof assistant tools which have been used by the educational community to introduce such concepts to students, but since these tools are not primarily created for educational purposes, students often do not benefit from them to the expected extent.

Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrated tangible impact that has inspired adoption in industry, their underlying semantics are less well-understood: what are "examples" and how do they relate to other kinds of specifications? This paper demonstrates that examples can, in general, be interpreted as refinement types. Seen in this light, program synthesis is the task of finding an inhabitant of such a type. This insight provides an immediate semantic interpretation for examples. Moreover, it enables us to exploit decades of research in type theory as well as its correspondence with intuitionistic logic rather than designing ad hoc theoretical frameworks for synthesis from scratch. We put this observation into practice by formalizing synthesis as proof search in a sequent calculus with intersection and union refinements that we prove to be sound with respect to a conventional type system. In addition, we show how to handle negative examples, which arise from user feedback or counterexample-guided loops. This theory serves as the basis for a prototype implementation that extends our core language to support ML-style algebraic data types and structurally inductive functions. Users can also specify synthesis goals using polymorphic refinements and import monomorphic libraries. The prototype serves as a vehicle for empirically evaluating a number of different strategies for resolving the nondeterminism of the sequent calculus---bottom-up theorem-proving, term enumeration with refinement type checking, and combinations of both---the results of which classify, explain, and validate the design choices of existing synthesis systems. It also provides a platform for measuring the practical value of a specification language that combines "examples" with the more general expressiveness of refinements.

Institutions small and large often use student teaching assistants (TAs) to provide office hours, tutor students, and grade student work, and the quality of a course's TAs can greatly affect the quality of the course. In this BOF we will discuss the training we provide to prepare TAs for their course duties and the mentoring we provide to foster their role as future educators. Improving the effectiveness of TA training and mentoring can have an immediate impact on the quality of teaching, potentially improve retention and diversity in computer science, and have a long-term impact on all aspects of our field as our current students and TAs progress through their industry and academic careers. Our goal is to provide a forum for you to disseminate your TA mentoring practices and for you to hear the mentoring practices of others, with the goal to develop a collection of best practices for TA training and mentoring for computer science. This BOF is appropriate for professors or instructors of any computer science course or summer program that uses undergraduate or graduate student teaching assistants.

No abstract available.

This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input–output examples to prune the search space. The algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs.

A great CS assignment is a delight to all, but the path to one can be most roundabout. Many CS students have had their characters built up on assignments that worked better as an idea than as an actual assignment. Assignments are hard to come up with, yet they are the key to student learning. The Nifty Assignments special session is all about promoting and sharing the ideas and ready-to-use materials of successful assignments.

Induction is a notoriously difficult topic for beginning computer science students to understand. Even if they can produce an inductive proof of some mathematical fact, many students never see the relevance of inductive reasoning outside of the classroom for anything beyond the natural numbers. This is unfortunate because inductive reasoning is closely intertwined with algorithm design and one of the cornerstones of reasoning about (recursive) programs. With the adoption of functional programming into the CS curricula core, it is a good time to revisit how we teach induction and try to make more explicit this fundamental connection between inductive reasoning and recursive programming. In this BoF session, we will discuss curriculum, strategies, and fun examples for teaching induction with an eye towards giving induction tangible and practical relevance for the computer science undergraduate.

The C++ programming language remains widely used, despite inheriting many unsafe features from C---features that often lead to failures of type or memory safety that manifest as buffer overflows, use-after-free vulnerabilities, or abstraction violations. Malicious attackers can exploit such violations to compromise application and system security.