1/2021

GTC/UnB + EFFA/UFG joint seminar

Zoom Link:

https://us02web.zoom.us/j/89412679078?pwd=ZjV6b3BvaGYwNFVLWXJaTWd6TjVWZz09

Meeting ID: 894 1267 9078

Passcode: 310030

Abstract. : Set theory has long been viewed as a foundation of mathematics, is pervasive in mathematical culture, and is explicitly used by much written mathematics. Because arrangements of sets can represent a vast multitude of mathematical objects, in most set theories every object is a set. This causes confusion and adds difficulties to formalising mathematics in set theory. We wish to have set theory's features while also having many mathematical objects not be sets.

A generalized set theory (GST) is a theory that has pure sets and may also have non-sets that can have internal structure and impure sets that mix sets and non-sets. This paper provides a GST-building framework. We show example GSTs that have sets and also:

- non-set ordered pairs,

- non-set natural numbers,

- a non-set exception object that cannot be inside another object

- modular combinations of these features.

We show how to axiomatize GSTs and how to build models for GSTs in other GSTs.

Meeting Link: https://meet.google.com/ben-bcwy-okz

Abstract. : Nominal techniques were created by Gabbay and Pitts [1] to deal with names and bindings in the syntax and semantics of formal languages. One of its applications involves the paradigmatic language of first-order logic. Using nominal techniques -- specifically, nominal sets and nominal algebra -- Gabbay and Mathijssen [2, 3] axiomatised the notion of substitution and first-order logic (just as traditionally we axiomatise Boolean algebra, groups, rings, fields, etc.). Later, Gabbay and Dowek [4,5] developed an abstract nominal lattice-theoretic semantics for these axiomatisations. This semantics provides a nominal generalisation of the usual notions of lattice theory. In this presentation we will explore the main notions involved in this construction, making a parallel between the usual and nominal notions of the theory of lattices.

Bibliography

1. Murdoch J. Gabbay and Andrew M. Pitts. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing, 13, pp. 214--2240, 2001.

2. Murdoch J. Gabbay and Aad Mathijssen. One-and-a-half-order logic. Proceedings of the 8th ACM- SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2006), ACM, pp. 189–-200, 2006.

3. Murdoch J. Gabbay and Aad Mathijssen. Capture-avoiding substitution as a Nominal Algebra. Formal Aspects of Computing, 20, pp. 451--479, 2008.

4. Murdoch J. Gabbay and Gilles Dowek. Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits. Proceedings of the 9th Italian Convention on Computational Logic (CILC 2012), CEUR workshop proceedings, 857, 2012.

5. Murdoch J. Gabbay. Semantics out of context: nominal absolute denotations for first-order logic and computation. Journal of the ACM, 63, pp. 1--66, 2016.

Abstract. : Since the early days of the termination competition, there have always been wrong answers produced by termination analysis tools. One way to increase the reliability of the generated analyses is by certification, an approach where the answers of the termination tools are checked by some verified certifier.

This talk will cover an overview of the CeTA certifier, whose soundness has been proven in Isabelle/HOL. We will start with the early phase where CeTA was solely used to check termination proofs of term rewrite systems, and then continue with recent developments that triggered the development of a fully verified SMT solver for linear integer arithmetic.

Abstract. : This talk discusses how we have modified Stickel's seminal AC-unification algorithm to avoid mutual recursion and formalised its termination and soundness in the PVS proof assistant. Furthermore, we discuss how Fages' termination proof of Stickel's algorithm was adapted, providing a unique elaborated measure that guarantees termination of the modified AC-unification algorithm. To the best of our knowledge, ours is the first formalised AC-unification algorithm for which soundness has been proved. Thus, our formalisation is the first step towards a formally verified sound and complete AC-unification algorithm.

Abstract. : The anti-unification problem is concerned with finding the least general generalization of a couple of terms, say s and t. In other words, it is the problem of finding a term r that could “represent” either both terms via substitutions σ and σ', that is, σr = s and σ'r = t. In this talk, we will present the anti-unification problem modulo the empty, associative, and commutative equational theories. We will show the simplification rules of each of these cases and discuss them by examples, pointing out the different results obtained for each equational theory. The purpose is to analyse the termination, confluence, and correctness properties of the anti-unification algorithms.

Abstract. : Assistentes de prova baseados em tipos dependentes (e.g. Coq e Lean) são ferramentas poderosas para se construir softwares corretos. No entanto, para se verificar programas escritos em uma linguagem diferente, é necessário construir uma representação deste programa no assistente de prova.

Quando a linguagem original do programa é similar o suficiente com a linguagem do assistente de prova, podemos utilizar uma técnica conhecida como shallow embedding para representar estes programas de forma direta na linguagem do assistente de prova. Um dos problemas desta abordagem é que qualquer diferença entre a semântica destas linguagens precisa ser levado em conta.

Nesta palestra apresento swaddling, uma técnica de mixed-embedding que nos permite modelar GADTs em OCaml como Inductive Datatypes em Coq. Esta técnica nos permite traduzir a riqueza de informação embutido na tipagem de GADTs sem perder a expressividade de pattern matching com impossible branches e sem recorrer ao uso de axiomas adicionais. Nós integramos esta técnica em coq-of-ocaml, uma ferramenta utilizada para traduzir automaticamente programas de OCaml para Coq. E demonstramos a utilidade de nossa abordagem utilizando esta implementação para traduzir para Coq uma porção da base de códigos da cryptomoeda Tezos.

Podcast: Type Theory for All

Twitter: https://twitter.com/p_droabreu0

Substructural Type Systems and Intersection Types

Mário Florido (Universidade do Porto)

Abstract. Types are now widely used as specifications for correctness properties of programs. However the standard type systems in use are usually not powerful enough to specify properties which limit the ordering and the number of uses of computational resources. Substructural type systems give us this extra power of controlling the number and order of uses of computational resources. Intersection types originate in the works of Barendregt, Coppo and Dezani and give us a characterization of the strongly normalizable terms, in the sense that a term is typed in an intersection type system if and only if it is strongly normalizable. These systems type more terms than the Curry type system and the Damas-Milner type system.

In this talk we will address the following problem: to which extent can we approximate a typed term in the intersection type system by terms typable in a simpler type system, such as the Curry Type System or a substructural type system? We will present a notion of term expansion, which generalises expansion as used before to linearize the strongly normalizable terms. Under this notion we will show that one can define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. We will then show that expansion relates terms typed by an intersection type with terms typed in the Curry Type System and several substructural type systems, tuning the degree of sharing by choosing different algebraic properties of the intersection operator.

Anti-unificação e semi-anéis

Andres González (PPG-MAT, University of Brasília)

Abstract. Unificação é o processo algorítmico de solução de equações entre duas expressões simbólicas, substituindo certas sub-expressões (variaveis) com outras expressões [Tob98]. Por outro lado Anti-unificação é o processo de generalizar duas expressões simbólicas, achando subexpressões comuns que compartilham as duas expressões. Anti-unificação é o processo dual da unificação. Além disso o problema de anti-unificação sobre algumas teorias equacionais como a teoria U2 unitária com dos símbolos de função [CK20] é de tipo zero ou nulo, é dizer que não existe um conjunto mínimo completo de generalizações. Nesta apresentação se extenderá este resultado de nularidade para a teoria de semi anéis como é mostrado em [Cer20]. Por último os problemas de anti-unificação tem sido usados para procurar funções paralelas recursivas [BBH18]; para prevenir bugs e configurações perdidas no software [MBK+20]; encontrar código duplicado ou similaridades no mesmo e detectar clonagem de códigos.

References

[BBH18] Adam D. Barwell, Christopher Brown, and Kevin Hammond. Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification. Future Gener. Comput. Syst., 79:669–686, 2018

[Cer20] David M. Cerna. Anti-unification and the Theory of Semirings. Theoretical Computer Science, 848:133–139, 2020.

[CK20] David M. Cerna and Temur Kutsia. Unital Anti-unification: Type Algorithms. 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), 167(6):26:1–26:20, 2020.

[MBK+20] Sonu Mehta, Ranjita Bhagwan, Rahul Kumar, Chetan Bansal, Chandra Maddila, B. Ashok, Sumit Asthana, Christian Bird, and Aditya Kumar. Rex: Preventing bugs and misconfiguration in large services using correlated change analysis. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 435–448, Santa Clara, CA, February 2020. USENIX Association.

[Tob98] Tobias Nipkow and Franz Baader. Term Rewriting and All That. CUP, 1998

Zoom Link:

https://us02web.zoom.us/j/89412679078?pwd=ZjV6b3BvaGYwNFVLWXJaTWd6TjVWZz09

Meeting ID: 894 1267 9078

Passcode: 310030

Functional Tuple Pairs and Applications to Higher-Order Complexity Theory

Deivid Vale (Radboud University Nijmegen)

Abstract. In this talk we discuss early developments of functional tuple pairs, i.e., an interpretation method for higher-order rewriting and functional programming. The main goal of this technique is thought to be twofold: first, we show how tuple interpretation subsumes earlier interpretation techniques and might be used in combination of classic methods like dependency pairs and rule removal; this is already the case in first-order rewriting. Second, we use tuple interpretations as a way to express runtime complexity for higher-order algebraic systems discussing a proper higher-order notion of program-data. We show that under mild assumptions we can derive complexity bounds for closed higher-order programs. We also show preliminary results on those interpretations being used as a main technique in implicit complexity theory as we might be able to capture higher-order functional complexity classes, for instance, the class of Basic Feasible Functionals (BFFs).

Zoom Link:

https://us02web.zoom.us/j/89412679078?pwd=ZjV6b3BvaGYwNFVLWXJaTWd6TjVWZz09

Meeting ID: 894 1267 9078

Passcode: 310030

2/2020

GTC/UnB + EFFA/UFG joint seminar

Reunião Zoom

https://us02web.zoom.us/j/89412679078?pwd=ZjV6b3BvaGYwNFVLWXJaTWd6TjVWZz09

ID da reunião: 894 1267 9078

Senha de acesso: 310030

Encoding Tight Typing in a Unified Framework

Prof. Andrés Viso (Univ. Nacional de Quilmes, LoRel team)

Abstract. This joint work with Delia Kesner explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a tight type system for CBPV. All such systems are quantitative, in the sense that they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of sequences to normal forms are discriminated according to their multiplicative/exponential nature, a concept inherited from linear logic.

Slides

Strong Call-by-Need

Prof. Thibaut Balabonski (Univ. Paris-Saclay, LRI, VALS team)

Abstract. Call-by-need is an evaluation strategy for the lambda-calculus, which models computation in lazy functional programming languages. Its defining feature is ensuring that each argument of a function is evaluated only once, and only if its value is actually needed.

As any other evaluation strategy, call-by-need is mainly concerned with producing values. As such it only performs weak reduction, that is it never reduces inside a lambda-abstraction. On the other hand, other applications based on the lambda-calculus like partial evaluators or proof assistants require computing normal forms, rather than simply values. For this they need strong reduction.

This talk introduces a calculus that enforces the principles of call-by-need evaluation while allowing strong reduction. The calculus is sound and complete with respect to usual beta-reduction: it computes the same normal forms as the lambda-calculus, in a by-need fashion. I will also relate how formalizing the calculus in a proof assistant (here: Abella) led to significant improvements in the pen-and-paper definitions.

Slides

Realizability in the unit sphere

Prof. Alexandre Miquel (Universidad de la República - Montevideo)

Abstract. The linear-algebraic lambda calculus is an extension of the lambda calculus where lambda terms are closed under linear combinations over a semiring K. For instance, if t and s are two lambda terms, then so is α.t + β.s with α, β ∈ K. The original motivation for such a calculus was to set the basis for a future quantum calculus, where α.t + β.s could be seen as the generalization of the notion of quantum superposition to the realm of programs (in which case K is the field C of complex numbers). In this talk, we shall present a semantics for the linear algebraic lambda-calculus, that is based on realizability (a technique initially introduced in Logic by Kleene in 1945). We shall see that this semantics, in which types are interpreted as subsets of some (infinite dimensional) unitary sphere allows us to capture those functions preserving the l2-norm, thus answering a long standing issue. From this, we derive a set of typing rules for a simply-typed linear algebraic lambda-calculus.

Foundations on Nominal Techniques

Ali Khãn Ribeiro (MAT-UnB)

Quantitative Types for Pair-Patterns

Profa. Sandra Alves (UPorto)

Abstract. In this talk, we explore recent approaches to quantitative typing systems for programming languages with pattern matching features. Quantitative (non-idempotent intersection) types have been used to characterise solvability for a pair pattern calculus, in which a qualitative characterisation of head-normalisation was given by means of typability. We show that one can go further and provide upper-bounds/exact measures for head-normalisation, by means of two resource-aware quantitative type systems (system U and system E), which takes advantage of specific technical tools. While system U provides upper bounds for the length of head-normalisation sequences and the size of normal forms, system E goes even further and produces exact measures for each of them, as well as discriminating between the different kinds of reduction steps performed