We explore the contributions of Alfonso Caracciolo di Forino, 1925–1996, to the creation of a school of formal methods in Italy, focusing on the problem of the formal definition of programming languages, including the semantic and pragmatic levels. In particular, we present his search for metalanguages and methods that could be used to give a “declarative definition” of a programming language. This research led him to the introduction of Generalized Markov Algorithms (GMAs), which extend Markov’s Normal Algorithms with metalinguistic variables, computable functions, and conditional applicability. For Caracciolo, a language definition was a GMA that, given a string, either rejects it if it is not a legal program or gives its meaning as a state-transforming function, thus taking care of the syntax (both context-free and context-dependent aspects) and semantics of the language, including non-terminating computations. Caracciolo’s group applied GMAs to several language definitions, to a complete simulation of the formalism used by the IBM Vienna Research Center to define PL/I, and, more generally, to the definition and simulation of dynamical systems. We contextualize these contributions in the Italian computing environment of the late 1950s and 1960s.

Programming has been considered the "essence of informatics" since the beginning of computing as a discipline. But programming in the fifties was very different from what we know today, and one of the goals (or dreams) throughout the history of programming language technology, has been "automatic programming''---the ability to automatically generate computer code starting from a high(er)-level description of the specification of that code. What this meant changed over the years, from punching paper tape, to compiling high-level programming languages, to program synthesis.

We present a learning path on cryptography for primary school students (Grade 5), which we designed and tested.The project aims to raise initial awareness of the core ideas of modern cryptography, which are fundamental concepts for becoming informed and active citizens in modern digital society.For this reason, we designed a progression of unplugged activities (sometimes integrated with task-specific, block-based programming environments) to expose students to different cryptographic techniques, where each new activity is motivated by an analysis of the criticalities encountered previously.We used unplugged activities to show that Computer Science (CS) does not necessarily imply the use of digital devices and to allow students to focus on its general scientific principles.We describe the designed learning module, discuss the main hinges in the experiment, and reflect on the lessons learned.The final evaluation showed excellent learning outcomes and high satisfaction with the activities.As cryptography uses mathematical tools (e.g., modular arithmetic, statistics), some parts of which are within reach of primary school children but rarely taught to them, it was possible to dwell on these aspects, making them experience mathematical objects in a non-standard context, and also stimulating a greater awareness of the impact of mathematics and CS in everyday life.

We report our experience of an extracurricular online intervention on cryptography in Grade 10. Our first goal is to describe how we taught some fundamental cryptography ideas by making students encounter a progression of representative cryptosystems, from classical to modern, and discover their characteristics and limitations. We used Snap! (a visual programming language) to realize hands-on activities: block-programming playgrounds (a form of task-specific programming languages) to experiment with cryptosystems, and an interactive app to support an unplugged (albeit remote) Diffie-Hellman key agreement. After experimenting with each system, the students were involved in a Socratic discussion on how to overcome the discovered limitations, motivating the introduction of the following system in our path. Our second goal is to evaluate the students' perceptions and learning of cryptography core ideas. They appreciated the course and felt that, despite being remote, it was fun and engaging. According to the students, the course helped them understand the role of cryptography, CS, and Math in society and sparked their interest in cryptography and CS. The final assessment showed that the students well understood the cryptography ideas addressed. Our third goal is to discuss what worked and areas of improvement. The "remote-unplugged" Diffie-Hellman, where the meeting chat was a metaphor for the public channel, engaged the students in understanding this groundbreaking protocol. Overall, they praised the activities as engaging, even when challenging. However, a strong "instructor blindness" induced by remote teaching often prevented us from giving the students the right amount of guidance during the exploration activities.

This poster illustrates how we redesigned the CS1 course for Math undergraduates to be held online but reflecting the face-to-face (F2F) experience as much as possible. We describe the course structure and the strategies we implemented to maintain the benefits of a synchronous experience. We present the positive and negative aspects that emerged from the students' opinion analysis. We highlight what worked, what did not, and what can be improved to strengthen the perception of a F2F experience and mitigate the "presence paradox" we found: although students are enthusiastic about the online format, most would still prefer a F2F course.

We extend to natural deduction the approach of Linear Nested Sequents and of 2-Sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction: only one introduction and one elimination rule per connective, no additional (structural) rule, no explicit reference to the accessibility relation of the intended Kripke models. We give systems for the normal modal logics from K to S4. For the intuitionistic versions of the systems, we define proof reduction, and prove proof normalization, thus obtaining a syntactical proof of consistency. For logics K and K4 we use existence predicates (à la Scott) for formulating sound deduction rules.

We show that the techniques for resource control that have been developed by the so-calledlight logicscan be fruitfully applied also to process algebras. In particular, we present a restriction of higher-order π-calculus inspired by soft linear logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

No abstract available.

We propose a type inference algorithm for lambda terms in elementary affine logic (EAL). The algorithm decorates the syntax tree of a simple typed lambda term and collects a set of linear constraints. The result is a parametric elementary type that can be instantiated with any solution of the set of collected constraints.We point out that the typeability of lambda terms in EAL has a practical counterpart, since it is possible to reduce any EAL-typeable lambda terms with the Lamping's abstract algorithm obtaining a substantial increase of performances.We show how to apply the same techniques to obtain decorations of intuitionistic proofs into linear logic proofs.

In 1998 Asperti and Mairson proved that the cost of reducing a lambda-term using an optimal lambda-reducer (a la Lévy) cannot be bound by any elementary function in the number of shared-beta steps. We prove in this paper that an analogous result holds for Lamping’s abstract algorithm. That is, there is no elementary function in the number of shared beta steps bounding the number of duplication steps of the optimal reducer. This theorem vindicates the oracle of Lamping’s algorithm as the culprit for the negative result of Asperti and Mairson. The result is obtained using as a technical tool Elementary Affine Logic. Key words: complexity, elementary affine logic, graph rewriting, optimal reduction

System F is a well-known typed λ-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F, called F<: (pronounced ef-sub), that combines parametric polymorphism with subtyping. The main focus of the paper is the equational theory of F<:, which is related to PER models and the notion of parametricity. We study some categorical properties of the theory when restricted to closed terms, including interesting categorical isomorphisms. We also investigate proof-theoretical properties, such as the conservativity of typing judgments with respect to F. We demonstrate by a set of examples how a range of constructs may be encoded in F<:. These include record operations and subtyping hierarchies that are related to features of object-oriented languages.

Abstract We present a sequent calculus for the modal logic S4, and building on some relevant features of this system (the absence of contraction rules and the confinement of weakenings into axioms and modal rules) we show how S4 can easily be translated into full prepositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities (exponentials) only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.

Abstract We present a translation of Ada configuration constructs, in a higher order, impredicatively typed, functional language (HOTFUL) with subtypes. The aim of this work is to provide an expressive executable semantics for Ada configuration constructs, and to verify the suitability of the chosen HOTFUL for such a task. In particular, we address the practicability of the approach when dealing with the development of a whole complex system, as well as the description of single modular units. After giving the detailed rules for the translation, we compare our approach with what could be obtained selecting a different typed language as “target”, namely the predicative type system of Standard ML.

The notions of weak Cartesian closed category and very weak CCC are introduced by dropping the extensionality (and the naturality) requirements in the adjunction defining the closed structure of a CCC. A number of specific examples of these categories are given. The weak notions are shown to be equivalent from both the semantic and syntactic standpoint to the typed non-extensional lambda-calculus and to the typed Combinatory Logic, extended with surjective pairs. Type-free models are characterized as reflexive objects in wCCCs. Finally, categorical models for the second-order non-extensional calculus are defined, by introducing a simple generalization of the notion of PL-category.