Even with the assistance of computer tools, the formalized de-scription and verification of research-level mathematics remains a daunting task, not least because of the talent with which mathema-ticians combine diverse theories to achieve their ends. By combin-ing tools and techniques from type theory, language design, and software engineering we have managed to capture enough of these practices to formalize the proof of the Odd Order theorem, a landmark result in Group Theory.

This panel will discuss what characterizes the publication process in the software engineering community and debate how it serves the needs of the community, whether it is fair - e.g. valuable work gets published and mediocre work rejected - and highlight the obstacles for young scientists. The panel will conclude with a discussion on suggested next steps.

Since Turing, we have wanted to use computers to store, process, and check mathematics. However even with the assistance of modern software tools, the formalization of research-level mathematics remains a daunting task, not least because of the talent with which working mathematicians combine diverse theories to achieve their ends. By drawing on tools and techniques from type theory, language design, and software engineering we captured enough of these practices to formalize the proof of the Odd Order theorem, a landmark result in Group Theory, which ultimately lead to the monumental Classification of finite simple groups. This involved recasting the software component concept in the setting of higher-order, higher-kinded Type Theory to create a library of mathematical components covering most of the undergraduate Algebra and graduate Group Theory syllabus. This library then allowed us to write a formal proof comparable in size and abstraction level to the 250-page textbook proof of the Odd Order theorem.

Abstract Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics , which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself. We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures , which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.

Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.

Adopting a programming-language perspective, we study the problem of implementing authentication in a distributed system. We define a process calculus with constructs for authentication and show how this calculus can be translated to a lower-level language using marshaling, multiplexing, and cryptographic protocols. Authentication serves for identitybased security in the source language and enables simplifications in the translation. We reason about correctness relying on the concepts of observational equivalence and full abstraction.

Communications processing is an important part of distributed language systems with facilities such as RPC (remote procedure call) and RMI (remote method invocation). For security, messages may require cryptographic operations in addition to ordinary marshaling. We investigate a method for wrapping communications processing around an entity with secure local communication, such as a single machine or a protected network. The wrapping extends security properties of local communication to distributed communication. We formulate and analyze the method within a process calculus.

Communication in distributed systems often relies on useful abstractions such as channels, remote procedure calls, and remote method invocations. The implementations of these abstractions sometimes provide security properties, in particular through encryption. In this paper we study those security properties, focusing on channel abstractions. We introduce a simple high-level language that includes constructs for creating and using secure channels. The language is a variant of the join-calculus and belongs to the same family as the pi-calculus. We show how to translate the high-level language into a lower-level language that includes cryptographic primitives. In this translation, we map communication on secure channels to encrypted communication on public channels. We obtain a correctness theorem for our translation; this theorem implies that one can reason about programs in the high-level language without mentioning the subtle cryptographic protocols used in their lower-level implementation.

By adding reflexion to the chemical machine of Berry and Boudol, we obtain a formal model of concurrency that is consistent with mobility and distribution. Our model provides the foundations of a programming language with functional and object-oriented features. It can also be seen as a process calculus, the join-calculus, which we prove equivalent to the π-calculus of Milner, Parrow and Walker.

We describe and prove the correctness of a new concurrent mark-and-sweep garbage collection algorithm. This algorithm derives from the classical on-the-fly algorithm from Dijkstra et al. [9]. A distinguishing feature of our algorithm is that it supports multiprocessor environments where the registers of running processes are not readily accessible, without imposing any overhead on the elementary operations of loading a register or reading or initializing a field. Furthermore our collector never blocks running mutator processes except possibly on requests for free memory; in particular, updating a field or creating or marking or sweeping a heap object does not involve system-dependent synchronization primitives such as locks. We also provide support for process creation and deletion, and for managing an extensible heap of variable-sized objects.

J.-Y. Girard's original definition of proof nets for linear logic involves boxes. The box is the unit for erasing and duplicating fragments of proof nets. It imposes synchronization, limits sharing, and impedes a completely local view of computation. The authors describe an implementation of proof nets without boxes. Proof nets are translated into graphs of the sort used in optimal lambda -calculus implementations; computation is performed by simple graph rewriting. This graph implementation helps in understanding optimal reductions in the lambda -calculus and in the various programming languages inspired by linear logic.>

An axiomatic version of the standardization theorem that shows the necessary basic properties between nesting of redexes and residuals is presented. This axiomatic approach provides a better understanding of standardization, and makes it applicable in other settings, such as directed acyclic graphs (dags) or interaction networks. conflicts between redexes are also treated. The axioms include stability in the sense given by G. Berry (Ph.D. thesis, Univ. of Paris, 1979), proving it to be an intrinsic notion of deterministic calculi.>

Lamping discovered an optimal graph-reduction implementation of the λ-calculus. Simultaneously, Girard invented the geometry of interaction, a mathematical foundation for operational semantics. In this paper, we connect and explain the geometry of interaction and Lamping's graphs. The geometry of interaction provides a suitable semantic basis for explaining and improving Lamping's system. On the other hand, graphs similar to Lamping's provide a concrete representation of the geometry of interaction. Together, they offer a new understanding of computation, as well as ideas for efficient and correct implementations.