This poster explores the integration of Reverse Mathematics (RM) as an innovative educational approach for teaching Theoretical Computer Science (TCS) at the university level. Beginning with a historical perspective, from Euclidean reasoning to Turing's limits, it situates RM within the broader landscape of TCS education. Through a concrete classroom activity, this work illustrates how RM fosters computational thinking, sharpens formal awareness, and bridges the gap between algorithmic implementation and logical justification. By encouraging students to reflect on the axiomatic principles required to validate algorithms, RM enables them to reason critically about constructive mathematics of computation, proof theory, formal logic and program verification. The poster concludes with a discussion of related work, preliminary teaching results, ongoing research, and initiatives toward curricular integration.

The aim of this poster is to present and discuss a curricular methodology to introduce computability topics to social sciences and economics students during the study of their CS subjects in the first courses. These TCS topics give rise to algorithmic impossibility and computational undecidability results which serve to increase students' motivation in their CSE in relation to their university studies. In addition, it allows them to acquire paradoxical and computational thinking skills, with which to deepen and raise computability questions in later courses. To support the impact of the new methodology with evidence, we have analyzed preliminary student results.

Classroom examples of non-computable problems most often involve sets of Turing machines, which makes these problems too abstract and far divorced from real-world practice, so some students are turned off by the abstract nature of theoretical CS. In this paper, we explore the pedagogical connection of undecidability results in theoretical computing with similar (un)computability results in physics that have recently appeared. We argue that incorporating these new impossibility and undecidability results can increase students' interest in theoretical computing topics, as well as improve their understanding of the underlying science and mathematics.

In this poster we present ITT, and Interactive Tutoring Tool that allows teachers of a Compiler Design course to interactively guide the learning from the implementation of the main theoretical concepts on lexical, syntactic analysis, and syntax-directed translation. With the help of ITT, our students interact with the visualization of the automata underlying the implementation obtained by the compiler-writing tools. Preliminary results show the benefits of using ITT to improve their understanding of theoretical concepts from the interactive execution of the implementation, deepening and reinforcing the understanding of theory in relation to the code.

In this work, we propose an educational technique that allows to improve the learning of the main theoretical concepts of a Compiler Design course. Instead of starting from the theory, and then explaining to the students how the implementation is obtained in each of the phases of building a compiler, we propose to use as a starting point the implementation obtained by the students through the use of automatic code generation tools. With the help of an Interactive Tutoring System, we guide the learning of the main theoretical concepts from the implementation obtained, deepening and reinforcing their understanding of the theory in relation to the code. In this way, students are able to better relate both parts and apply them together, resulting in a more solid design of language processing tools. As a preliminary evaluation of the described technique, we show the results obtained by the students in the last courses.

The low academic results and mathematical difficulties experienced by students in learning theoretical computer science have been one of the reasons why many undergraduate students postpone the study of their theoretical subjects until absolutely necessary. For this reason, some optional theoretical subjects have been postponed for the last years, and in some cases, not included in the curricula due to lack of students. In order to reverse this problematic situation in theoretical computing education, it is essential that students acquire as soon as possible an intuitive and progressive knowledge of the main theoretical computing concepts and their associated skills and abilities. To achieve this goal, in this paper we offer a complete educational methodology to systematically introduce questions of computability and algorithmic complexity, in the early years of computer science and mathematics degrees, from the results of impossibility that are already included in the curriculum of CS-geared mathematics courses. To provide clear evidence of the impact of the applicability of the proposed methodology, we analyze the experimental results and student feedback we have obtained to confirm that the introduction of theoretical computing questions from impossibility results increases students' academic results in theoretical computing subjects, and motivation and interest in studying mathematical subjects of beginning level of computer science.

In this paper, we present a novel technique to systematically introduce questions of computability and algorithmic complexity in the curricula of the early years of Computer Science degrees. We propose to start from those results of impossibility that are already included in the curriculum of CS-geared mathematics courses, and around these classical impossibility theorems, we identify motivating and interesting theoretical computing questions. We provide a helpful list of impossibility results and motivating problems, and we analyze how and where they could be introduced in the CS mathematics curriculum. We also provide a preliminary evaluation of the effectiveness of the proposed technique to demonstrate that the introduction of theoretical computing questions from impossibility results could increase students' academic results in theoretical computing subjects and mathematics subjects of the CS curriculum.

This poster presents an Interactive Tutoring System (ITS) that allows teachers to tutor and evaluate interactively the learning process that the students of a Compiler Design course must experience from each theoretical concept to obtain the code of its corresponding implementation (scanners, parsers, translators, interpreters, compilers), regardless of the specific tools chosen for the automatic code generation and the programming language. Through the use of the ITS, each teacher will be able to select those tools that he/she considers more adequate for the development of the course, and integrate them modularly into a common educational environment, so that if later on she/he decides to change these tools or the programming language, the ITS will continue to be valid, and the tutoring and evaluation process carried out by the ITS will remain the same to guide the students from theory to implementation.

The purpose of this poster is to provide practical arguments to stimulate debate and discussion on whether or not to introduce concepts of theoretical computer science in the pre-university education system, conveniently adapted within students' capability. Theoretical computer science is a hard subject to teach at the university level. Many students who enter the computer sciences courses have very little mathematical or theoretical background. For this reason, it is important that students acquire an appreciation of these concepts before they leave the secondary education. In anticipation that these contents would not be included or addressed in the context of a subject of Computer Science, a work in progress educational experience is presented during the 2018-2019 academic year for enhancing the algorithmic curriculum of pre-university computing and mathematical courses. We describe a collection of selected problems, puzzles and riddles from high school mathematics and introductory logic, to be added to the current secondary curriculum. We want to show attendees the use of our educational activities, offering practical aspects that could not be shown through the reading of a paper, so that they can learn to use them in their own classes. The preliminary experimental results show that the students who have undergone this educational experience have obtained a higher motivation that those who have followed the course in its traditional form. We believe that introducing these theoretical computer concepts can help students to perform better in some areas of computer science and be increasingly prepared and motivated for their university studies.

This Work in Progress report presents an educational software tool for testing abstract data types implemented in C++ against formal algebraic specifications written in Maude, a formal specification language based on rewriting logic that allows the specification of abstract data types in a clear and concise manner. Maude specifications are executable, which provides two advantages: firstly, we can test our specifications and, secondly, we can obtain the results of the test cases automatically. Our software testing tool is fully integrated in the Eclipse programming environment and is platform-independent. We have developed an Eclipse plug-in that calls the Maude system to generate the test cases and translates them into a sequence of C++ instructions. The C++ instructions are compiled and executed, and the results are compared with the results obtained from the execution of the formal algebraic specification. Thus, the learning tool allows Software Engineering students to test their own implementations and correct their errors, encouraging the use of formal methods in their developments and resulting in an improved software quality.

While Computational Logic plays an important role in several areas of Software Engineering (SE), most of the educational technology developed for teaching logic ignores their application in a larger portion of the SE education domain. In this paper we describe an innovative methodology based on a prototype logic teaching tool on semantic tableaux to prepare and train the students to use logic as a formal proof technique in other topics of SE, such as the formal verification of algorithms and the declarative debugging of imperative programs, which are foundations of good development of software.

In this paper, we propose a new methodology based on a logic teaching tool on semantic tableaux that has been developed to help students to use logic as a formal proof technique in advanced topics of Computer Science, such as the formal verification of algorithms and the algorithmic debugging of imperative programs.

Modularity is a key issue in the construction of large multi-paradigm declarative programs involving complex features like higher-order, polymorphism or constraints. The modular framework defined in this paper for higher-order declarative constraint programming builds complex software systems by combining and composing existing components or modules from a number of composition operations expressive enough to model typical modularization issues like export/import relationships and inheritance. The effectiveness of our approach relies on a higher-order constraint rewriting logic over a parametrically given constraint domain as the basis of a model-theoretic and fixpoint semantics for program modules, and a modular semantics given by a suitable immediate consequence operator which is compositional and fully abstract, offering the possibility of reasoning on the composition process itself. The availability of this well-founded semantics characterization for structuring and modularizing higher-order declarative constraint programs provides the ground to perform sound semantics-based transformation, analysis, debugging and verification of declarative software.

We propose a higher-order logical framework for declarative programming as an extension to the setting of the simply typed lambda calculus of a first-order rewriting logic, where programs are now presented by conditional pattern rewrite systems on lambda abstractions. We use this new logical framework to obtain a natural model-theoretic semantics from traditional theories in higher-order declarative (functional and logic) programming, and we provide a fixpoint semantics that matches the pattern model of a program as the least fixpoint of an operator defined over pattern algebras. We use this higher-order semantic framework as a basis for the verification of declarative programs and the development of efficient algorithmic debugging techniques. Our debugging approach proceeds by exploring an abridged computational tree built on a higher-order proof calculus with lambda abstractions that provides a purely declarative view of the computation, in order to detect a function rule that is incorrect in the intended model of the program's semantics. For verification purposes, our higher-order logical framework can be mapped into higher-order logic programming, and we can use this translation as a starting point to explore how to prove properties valid in the least pattern model of a program by means of different existing interactive proof assistants, as the Isabelle theorem prover.

Abstract This paper presents a computational model for the cooperation of constraint domains and an implementation for a particular case of practical importance. The computational model supports declarative programming with lazy and possibly higher-order functions, predicates, and the cooperation of different constraint domains equipped with their respective solvers, relying on a so-called constraint functional logic programming (CFLP) scheme. The implementation has been developed on top of theCFLPsystem , supporting the cooperation of the three domains ℋ, ℛ, and ℱ , which supply equality and disequality constraints over symbolic terms, arithmetic constraints over the real numbers, and finite domain constraints over the integers, respectively. The computational model has been proved sound and complete w.r.t. the declarative semantics provided by theCFLPscheme, while the implemented system has been tested with a set of benchmarks and shown to behave quite efficiently in comparison to the closest related approach we are aware of.

This paper presents a computational model for the cooperation of constraint domains, based on a generic Constraint Functional Logic Programming (CFLP) Scheme and designed to support declarative programming with functions, predicates and the cooperation of different constraint domains equipped with their respective solvers. We have developed an implementation in the CFLP system TOY, supporting an instance of the scheme which enables the cooperation of symbolic Herbrand constraints, finite domain integer constraints, and real arithmetic constraints. We provide a theoretical result and an analysis of benchmarks showing a good performance with respect to the closest related approach we are aware of

Abstract In this paper, we present our proposal to Constraint Functional Logic Programming over Finite Domains (CFLP( $\fd$ )) with a lazy functional logic programming language which seamlessly embodies finite domain ( $\fd$ ) constraints. This proposal increases the expressiveness and power of constraint logic programming over finite domains (CLP( $\fd$ )) by combining functional and relational notation, curried expressions, higher-order functions, patterns, partial applications, non-determinism, lazy evaluation, logical variables, types, domain variables, constraint composition, and finite domain constraints. We describe the syntax of the language, its type discipline, and its declarative and operational semantics. We also describe \toy(fd)$ , an implementation forCFLP( $\fd$ ), and a comparison of our approach with respect toCLP( $\fd$ ) from a programming point of view, showing the new features we introduce. And, finally, we show a performance analysis which demonstrates that our implementation is competitive with respect to existingCLP( $\fd$ ) systems and that clearly outperforms the closer approach toCFLP( $\fd$ ).

The new generic scheme CFLP (D) has been recently proposed in [24] as a logical and semantic framework for lazy constraint functional logic programming over a parametrically given constraint domain D. In this paper we extend such framework with a suitable operational semantics, which relies on a new constrained lazy narrowing calculus for goal solving parameterized by a constraint solver over the given domain D. This new calculus is sound and strongly complete w.r.t. the declarative semantics of CFLP (D)programs, which was formalized in [24] by means of a Constraint Rewriting Logic CRWL (D).

We propose a demand-driven conditional narrowing calculus in which a variant of definitional trees [2] is used to efficiently control the narrowing strategy. This calculus is sound and strongly complete w.r.t. Constructor-based ReWriting Logic (CRWL) semantics [7] for a wide class of constructor-based conditional term rewriting systems. The calculus mantains the optimality properties of the needed narrowing strategy [5]. Moreover, the treatment of strict equality as a primitive rather than a defined function symbol, leads to an improved behaviour w.r.t. needed narrowing.