LMF PhD Seminars

I will present some history and applications of defunctionalization. We will see how this technique for compiling closures can also be a useful programming technique, making boring programming languages more fun.

The diversity of output encodings of different reasoning systems hinders proof verification and interoperability. The Dedukti framework addresses this issue by implementing the λΠ-calculus modulo, enabling proofs from different frameworks to be expressed, combined, and checked automatically.
 However, the formal verification of fully automated higher-order logic provers remains an unmet challenge, and extending state-of-the-art provers with this capability is particularly difficult due to the numerous complex rules typically implemented in these systems. Moreover, provers can introduce variations in proof formulas that are not caused by the underlying calculus rules but by specific implementation details, requiring additional verification steps.
In this talk, I will outline the key challenges and requirements for verifying such systems and present a modular encoding approach designed to support the systematic derivation of encodings for both calculus rules and prover-specific proof steps. I will also report on ongoing work applying this approach to the higher-order logic prover Leo-III.

In this talk, I will present a decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. The method is based on a model-based translation to SMT for which we introduce several optimisations–the most important of them is based on bounding the size of predicate instantiations within models of larger formulae, which leads to a much more efficient translation of SL formulae to SMT. I will also briefly discuss ongoing research to generalise the decision procedure for user-defined inductive data structures.

In this talk, I will present the general idea of lattice formulation of quantum field theories and show how and where the fermion doubling occurs. Then I will give an example of FD on quantum cellular automaton along side with the solution of the problem, which defines a modification on the lattice via flavor symmetry. Then I will conclude with the generalizations of FD with the use of Riemann-Hurtwitz formula and Poincare-Hopf theorem

<abstract>

Lean is a proof assistant developed by the Lean FRO that has become especially popular with mathematicians in recent years, whose type-theoretic foundations take after the proof assistant Coq. It introduces a number of additional definitional equalities, particularly those of proof irrelevance and K-like reduction, which are great conveniences for mathematical formalization but complicate metatheoretical analyses and the task proof export. To translate Lean proofs to a smaller theory "Lean-" with fewer such definitional equalities, we implement a special case of the extensional-to-intensional translation that injects type casts using generated equality proofs that are typeable in Lean-. We have modified "Lean4Lean", a port of Lean's typechecker kernel to Lean, to effect our translation by "patching" terms in parallel to typechecking, resulting in a translation implementation that we call "Lean4Less".

Lean4Less is able to successfully translate certain libraries of limited size in Lean, such as the standard library and some lower-level Mathlib modules, though work still remains to be done to scale the translation up to larger formalizations. As the translation framework implemented by Lean4Less should be consistent with a general extensional-to-intensional translation, this work could also be relevant to near-future developments in the Lean kernel/elaborator for enabling some limited forms of user-extensible extensional-like reasoning in Lean.

<abstract>

Random Walks are common tools in probabilistic computation, in some algorithmic context they allow us to spare the use of random ressources. In this introductory talk to Quantum Computation, I introduce them and their quantum analogous: Quantum Walks. I discuss in what sense do probabilistic and quantum computation differ, and I introduce on the way some key features of Quantum Computation (Measurement, Interferences, Reversibility ...).

Today we will learn to count! Following the steps of the mathematicians Agustín Rayo and Adam Elga, our goal will be to generate abominably large finite numbers ; not because we must, but because we can. On the way, we will learn various techniques like Knuth's arrows or the fast-growing hierarchy ; we will finally understand what is up with Graham's number ; and we will be able to name the biggest number ever (yes, for real).

Programming languages are designed with different goals. They are often complimentary, and can each be efficient for their own subset of problems. In practice, we would like to be able to mix them together. To do so, languages have to expose a way to communicate to each other, called FFI (Foreign Function Interface). Languages often have different memory models. To guarantee safety, very strict rules have to be enforced. We focus on interoperability between OCaml and C, and how formal methods can be used to guarantee the correct use of its rules.

Systems engineering requires to use many commercial modeling tools for which semantics is not always formally defined, if defined at all. Engineers have to adapt to the many different conceptions, and the relationships between the various models they develop are difficult to keep consistent over time. This work presents the simplified approach based on inductive type theory which is much simpler to deploy. We propose a Metamodel definition language based on small and effective formal basis, allowing to describe different models. With deep and shallow embedding in Coq we show how translation between Domain Specific Language (DSL) and formal description can be performed.

Computation can be introduced into proof systems using rewrite rules. It is convenient, as parts of the proofs are directly managed by the system. But do rewrite rules also add expresiveness? In other words, can we prove the same results with axioms instead of rewrite rules? We focus on the λΠ-calculus modulo theory, an extension of simply typed λ-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the λΠ-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof. To do so, we introduce a heterogeneous equality in the target theory, and we build a translation that replaces each use of the conversion rule by the insertion of a transport.

We often divide programming languages into two categories: those that are strongly-typed but rigid, and those that are more flexible but untyped (or dynamically typed). While static typing offers formal guarantees about the soudness of programs ("well-typed programs cannot go wrong") and can be used for the documentation and the tooling (auto-completion, etc), this often comes at the expense of flexibility, making programs more secure but prototyping more tedious. In this presentation, we study a formal system to statically type dynamic languages such as Python or Javascript, offering a compromise between safety and flexibility.

The static typing of dynamic languages raises new challenges. In particular, in dynamic languages, functions can be overloaded: they can express multiple behaviors that cannot be resolved statically, but instead are selected at runtime (dynamic dispatch). Some work aims to extend these languages with static typing (e.g. Typescript for Javascript), but lacks a formalization and an algorithm for infering type without needing annotations from the programmer.

To address this issue, we present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types, and subtyping. This yields a type discipline in which unannotated functions are given polymorphic types (thanks to Hindley-Milner) that can capture the overloaded behavior of the functions they type (thanks to the intersection types) and that are deduced by applying advanced techniques of type narrowing (thanks to union types). This makes the system a prime candidate to type dynamic languages.

<abstract>

We present a low-level language suitable for writing basic algorithms of computer algebra (e.g. algorithms from the GMP or BLAS libraries). Such algorithms primarily use arrays to represent most mathematical objects. Our language therefore focuses on arrays. We present the semantics of our language, which was formalized in Coq. This semantics is safe, that is, well-typed programs cannot run into an undefined behavior. Another goal for this semantics is simplifying proof of programs. In particular, it does not manipulates any memory, nor pointers, and aliases of mutable arrays are forbidden. Finally, we present the formally verified compiler for our language. To achieve this, the compiler translates programs written in our language to the C#minor intermediate language of CompCert and we formally proved that the semantics is preserved by this translation.

Dependent type theory is the logical foundation of many popular proof assistants, such as Coq, Agda and Lean. However, when presented in its most primitive form, the syntax of type theory suffers from a serious usability problem: every type annotation must be explicitly spelled out, rendering it unusable in practice. In order to solve this, usual presentations of type theory omit the majority of these annotations, but this has a cost. Because knowing them is still important when typing terms, it becomes unclear how to do this algorithmically.

A solution to this problem is provided by bidirectional typing, a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal.

In this talk I will give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which I define declarative and bidirectional type systems. I then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with various theories.