Unification modulo equational theories in languages with binding
operators (Slides, Talk related to Joint LOPSTR/PPDP 2023 Invited Talk
)
Maribel
Fernández (Deputy Head of Department (Academic Planning), Department of
Informatics, King’s College London)
14:00-16:00, Monday, May 13th 2024, Auditório do MAT
Abstract: Unification (i.e., solving equations between terms) is a key step in the implementation of logic programming languages and theorem provers, and is also used in type inference algorithms for functional languages and as a mechanism to analyse rewrite-based specifications (e.g., to find critical pairs). Matching is a version of unification in which only one of the terms in the equation can be instantiated. Often, operators satisfy equational axioms (e.g., associativity, commutativity), which must be taken into account during the unification or matching process. In addition, when the expressions to be unified involve binding operators (as is the case when representing programs, logics, computation models, etc.), unification and matching algorithms must take into account the alpha-equivalence relation generated by the binders. In this talk, we will discuss matching and unification algorithms for languages that include binding operators as well as operators that satisfy equational axioms, such as associativity and commutativity.
PVS hands-on!
Mariano Moscato
(Analytics Mechanics Associate AMS, NASA LaRC Formal Methods)
14:00-16:00, Monday, April 29th 2024, Sala multiusos ou LaForCE
(CIC/EST)
09:00-12:00, Friday, May 3rd 2024, Sala multiusos ou LaForCE (CIC/EST)
PVS files: quadratic, induction, binary_tree_nat, BinaryTreeNat, Expressions
PVS handout: Handout 01, Handout 02
Abstract: Brief course on intermediate to advanced concepts on
formalization and automated proving techniques using the Prototype
Verification System (PVS). It is planned as a hands-on activity, where
all concepts will be put in practice. Brainstorming on the
state-of-the art of PVS. The attendants will be encouraged to
participate and discuss about specialized knowledge on the recent
developments of PVS and opportunities of applications.
A Survey on Antiunification (Slides)
(Cerna and Kutsia's Related IJCAI-2023 survey)
Temur Kutsia
(RISC/Johannes Kepler University Linz)
10:00-12:00, Friday, March 22nd 2024, Auditório Matemática
Solving and Computing with Variadic Terms (Slides)
Temur Kutsia
(RISC/Johannes Kepler University Linz)
10:00-12:00, Friday, March 22nd 2024, Auditório Matemática
Vigésimo primeiro Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
Realizado como track em Lógica e Computação do
XVI Summer Workshop
in Mathematics
7-9 de Fevereiro 2024.
Final Program
Comitê
Científico: Thaynara Arielly de Lima (IME/UFG), Elaine Pimentel
(UCL).
Vigésimo Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
Com participação dos pesquisadores Temur Kutsia e
Mariano Moscato, visitantes no contexto do PrInt UnB CAPES dos PPGs em
Matemática e Informática.
10 Fevereiro 2023.
Final Program: Program
including talks and affiliated short courses by the Invited Speakers:
Nominal Matching Logic (Slides)
Maribel Fernández (King's College London)
09:00-10:00, Tuesday, November 1st 2022, Sala Multiusos CIC
Décimo Nono Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
organizado por Mauricio Ayala-Rincon, Temur Kutsia, and Daniele Nantes, como parte da Escola de Verão /
XIV Workshop de Matemática da UnB 2022 (XIV SWM 2022)
17-21 Jan 2022.
Final Program: Program
including talks by Invited Speakers:
Décimo Oitavo Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
organizado por Daniele Nantes, como parte da Escola de Verão /
XIII Workshop de Matemática da UnB 2021 (XIII SWM 2021)
08-11 Feb 2021.
Final Program: Program
including talks by Invited Speakers:
Décimo Setimo Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
organizado por Daniele Nantes, como parte da Escola de Verão /
XII Workshop de Matemática da UnB 2020 (XII SWM 2020)
10-14 Feb 2020.
Fotos: F1, F2, F3
Final Program: Program
including talks by Invited Speakers:
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Mariano Moscato
(National Institute of Aerospace NIA, Hampton, VA USA)
10:00-12:00, Friday, Nov 29th, 2019, Auditório CIC/EST
Abstract: The problem of determining whether or not a point lies inside a given polygon occurs in many applications. In air traffic management concepts, a correct solution to the point-in-polygon problem is critical to geofencing systems for Unmanned Aerial Vehicles and in weather avoidance applications. Many mathematical methods can be used to solve the point-in-polygon problem. Unfortunately, a straightforward floating-point implementation of these methods can lead to incorrect results due to round-off errors. In particular, these errors may cause the control flow of the program to diverge with respect to the ideal real-number algorithm. This divergence potentially results in an incorrect point-in-polygon determination even when the point is far from the edges of the polygon. This paper presents a provably correct implementation of a point-in-polygon method that is based on the computation of the winding number. This implementation is mechanically generated from a source-to-source transformation of the ideal real-number specification of the algorithm. The transformation soundly approximates Boolean expressions in conditional statements. The correctness of this implementation is formally verified within the Frama-C analyzer, where the proof obligations are discharged using the Prototype Verification System (PVS).
Décimo Sexto Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
organizado por Daniele Nantes, como parte da Escola de Verão / XI Workshop de Matemática da UnB 2019
Data: 21-22 Fev 2018
Locais: Auditórios Departamento de Matemática, UnB
Programa
Palestras convidadas proferidas por Alejandro Díaz-Caro
(UNQuilmes e UBA), Vander Ramos Alves (UnB), e membros do GTC.
Décimo Quinto Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
organizado por Daniele Nantes, como parte da Escola de Verão / X Workshop de Matemática da UnB 2018
Data: 21-22 Fev 2018
Locais: Auditórios Departamento de Matemática, UnB
Programa
Palestras convidadas proferidas por Edward Hermann Haeusler (PUC-Rio),
Mário Benevides (UFRJ), Bruno Lopes (IC/UFF) e Marcelo Finger
(IME/USP), e membros do GTC.
A Static Analysis Framework for the Estimation of Verified Floating-Point Round-Off Errors
Mariano Moscato
(National Institute of Aerospace NIA, Hampton, VA USA)
16:00-18:00, Tuesday, Oct 3rd, 2017, Auditório CIC/EST
Abstract: This talk is aimed to present a static analysis technique for computing formally verified round-off error bounds of floating-point functional expressions. The technique is based on a denotational semantics that computes a symbolic estimation of floating-point round-off errors along with a proof certificate that ensures its correctness. The symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. The proposed technique is implemented in the prototype research tool PRECiSA (Program Round-off Error Certifier via Static Analysis) and used in the verification of floating-point programs of interest to NASA.
PVS for computer Scientists (foils and PVS theories - PVS Class 2017)
César
Munoz, Mariano Moscato and Mauricio
Ayala-Rincón
25th September 2017, Mód 14 CIC/UnB
One-day tutorial Collocated with Tableaux/FroCoS/ITP
12th Logical and Semantic Frameworks with Applications - LSFA 2017 FINATEC/UnB, 23-24 Setember, 2017.
26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - Tableaux 2017 FINATEC/UnB, 25-28 Setember 2017.
11th International Symposium on Frontiers of Combining Systems FroCoS 2017 FINATEC/UnB, 27-29 Setember 2017.
8th International Conference on Interactive Theorem Proving ITP 2017 FINATEC/UnB, 26-29 Setember 2017.
On NP versus PSPACE and NP versus coNP link a material relacionado
Edward Hermann Haeusler
(PUC-Rio - Trabalho conjunto com Pawel Gordeev)
14:00-16:00, Friday, August 4th, 2017, Sala Múlti-usos CIC
Pure Type Systems: Extensions and Restrictions foils
Fairouz Kamareddine
(Heriot-Watt University, Edinburgh, UK)
10:00-11:20, Wednesday, May 24rd, 2017, Auditório MAT
Abstract: Pure Type Systems (PTSs) encompass all versions of Explicit type systems a la Church (from Simple types to polymorphic types to dependent types, to types with universes). Furthermore, PTSs have versions that elegantly represent Implicit type systems a la Curry, intersections, union and singleton types and subtyping. More importantly, PTSs allow the classification of type and proof theory strengths and have set theoretical versions. They can be used to characterise Church Rosser and Strong Normalisation (SN) and allow us to see where a property ceases to hold at which type theoretic level. For example, SN properties for the calculus of construction (CC) and and the polymorphic lambda calculus with constructor types (Fω) have the same proof-theoretic strength as higher-order arithmetic (HAω) although CC and Fω can be proven consistent within Heyting arithmetic. In this talk, I will discuss extensions and restrictions of PTS and explain the complexity of proofs of strong normalisation for various versions.
Décimo Quarto Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
organizado por Daniele Nantes, como parte da Escola de Verão / IX Workshop de Matemática da UnB 2017
Data: 14-15 Fev 2017
Locais: Auditórios Departamento de Matemática, UnB
Programa
Mini-cursos em "Isomorfismos Parciais", Rodrigo Freire (FIL/UnB), e
"Rewriting Logic in a Nutshell with Pecan Pie", Christinao Braga
(IC/UFF); Palestras convidadas proferidas por Rodrigo Freire (FIL/UnB),
Christiano Braga (IC/UFF), Hugo Mariano (IME/USP) e Francicleber Ferreira
(DCC/UFC), e membros do GTC.
Existência de Provas em Lógica
Proposicional link a material relacionado
Edward Hermann Haeusler
(PUC-Rio - Trabalho conjunto com Pawel Gordeev)
08:00-10:00, Friday, August 5th, 2016, Auditório MAT
Resumo: Discutimos o problema da existência de provas de tautologias proposicionais. Apresentamos uma abordagem para compactação de provas a partir de Dedução Natural e Grafos de prova. A aplicamos estes resultados teóricos na prova da conjectura NP = PSPACE e na existência de certificados polinomiais para grafos não-Hamiltonianos.
Aprendizado Exato de Ontologias em Lógica Descritiva foils
Ana Ozaki Rivera Castillo
(Ph.D. U. Liverpool)
16:00-17:00, Thursday, June 16th, 2016, Sala Multi usos do EST
Abstract: Ontologias tem sido utilizadas em diversos domínios da ciência, como medicina, química e biologia, para representar conhecimento conceitual de forma declarativa. O formalismo mais usado para especificação de ontologias é dado pela lógica descritiva (LD). Neste trabalho vemos o problema de construir uma ontologia como um problema de aprendizado e investigamos a complexidade de aprender uma ontologia em LD no modelo de aprendizado exato com consultas à um oráculo, desenvolvido por Angluin et al. Dado um conjunto de linguagens em LD, investigamos se existe um algoritmo que aprende uma ontologia em determinada linguagem em tempo polinomial.
Décimo Terceiro Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
organizado por Daniele Nantes, como parte da VII
XLV Escola de Verão / VIII Workshop de Matemática da UnB 2016
Data: 27-29 Jan 2016
Locais: Auditórios Departamento de Matemática, UnB
Programa
Mini-curso em "Tipos de Intersecção", Daniel Lima
Ventura (UFG); Palestras convidadas proferidas por Marcelo Finger
(USP), Vivek Nigam (UFPr/CG), Petrúcio Viana (UFF), Daniel
Ventura (UFG) e Bruno Lopes
(UFRJ) e membros do GTC.
Foils of the talks available:
"Multiset Rewriting
with Dense Times and the Analysis of Cyber-Physical Security
Protocols" by Vivek Nigam
"Induction,
iteration, recursion, and well orderings" by Petrúcio
Viana
"Practical
Reasoning, Inconsistency and Modelling" by Marcelo Finger
"Towards reasoning
about concurrency: a logical approach" by Bruno Lopes
"An Intersection Type System for Nominal Terms" by Ana Cristina Rocha-Oliveira
"Analisando Terminação:
Size Change Principle versus Dependency Pairs" by Ariane A. Almeida
"Formalização da Terminação de Especificções Funcionais" by Thiago M.F. Ramos
"A Formalisation of Nominal Equivalence with AC f-Symbols" by Washington R. de Carvalho Segundo
A Gentle Introduction to Process Calculi foils
Jorge A. Perez
(Johann Bernoulli Institute for Mathematics and Computer Science
University of Groningen, The Netherlands)
10:15-12:00, Monday, July 20th, 2015, Sala Multi usos do CIC
(Foils about the U. of Groningen)
Abstract: Nowadays, communication and concurrency are ubiquitous concepts in computing. Concurrent
systems involve multiple interacting agents (processes); often infinite, these interactions are hard to describe
and analyze. These features are in sharp contrast with those of sequential programs which are typically
characterized by finite, deterministic computations. Process calculi are formal specification languages for
concurrent systems. They define core programming languages in which concurrent, communicating systems
can be rigorously specified and reasoned about, following a compositional approach. This talk offers a brief
introduction to the specification and analysis of concurrent systems using process calculi. I will present the
main concepts of Milner's CCS (Calculus of Communicating Systems), one of the most representative
process calculi. The syntax, semantics, and reasoning techniques for CCS will be presented. Also, basic
notions of the pi-calculus (the extension of CCS for mobile
communication) will be briefly introduced
Curry-Howard Correspondence for Concurrency foils
Jorge A. Perez
(Johann Bernoulli Institute for Mathematics and Computer Science
University of Groningen, The Netherlands)
09:00-12:30, Tuesday, July 21st, 2015, Sala Multi usos do CIC
Abstract: A central concept in the theory of programming languages is the so-called Curry-Howard
correspondence: it tightly relates, on the one hand, logical propositions and types; on the other hand, it
connects proofs and functional programs. This correspondence has proved essential to endow reasoning
techniques over sequential programs with principles which have both operational and logical meanings. In
2010, Caires and Pfenning put forward an interpretation of linear logic propositions as session types for
communicating processes. Remarkably, this result defines a propositions-as-types/proofs-as-programs
correspondence, in the style of the Curry-Howard correspondence, but in the context of concurrent processes
defined in the pi-calculus. In this talk, I will give an overview to session types for concurrency and to Caires
and Pfenning's interpretation. If time permits, I will also present some associated developments for this
interpretation: logical relations, typed behavioral equivalences, and type isomorphisms.
Expressiveness in Concurrency foils
Jorge A. Perez
(Johann Bernoulli Institute for Mathematics and Computer Science
University of Groningen, The Netherlands)
10:30-12:00, Monday, July 27st, 2015, Sala Multi usos do CIC
Abstract: One fundamental issue in the theory of process calculi concerns their relative expressiveness. In
this setting, one typical problem is, e.g., understanding whether two process calculi are equally expressive -
that is, whether they express the exact same class of concurrent behaviors. Also, one may be interested in
establishing the contribution of a particular process construct to the overall expressivity of a given process
language. Yet another application of relative expressiveness is the transference of reasoning techniques
between different process languages. Establishing formal relationships between calculi in terms of their
expressive power is a challenging endeavor, as it entails developing formal principles for language
translations and their correctness criteria. Depending on the process calculus at hand, the criteria may vary,
or certain criteria could be more useful than others. In this talk, I will give an overview to research in
relative expressiveness for process calculi. I will illustrate main notions and approaches by presenting
classic expressiveness results for CCS and the pi-calculus. I will also discuss current challenges and open
problems, in particular expressiveness of process calculi with rich type disciplines, such as session types.
Mini-curso: Selected Topics in Unification Theory
Temur Kutsia
(RISC - Johannes Kepler University Linz)
10:00-12:00, Wednesday, April 1st, 2015, Auditório MAT UnB
Foils: Selected Topics in Unification Theory
10:00-12:00, Tuesday, April 7th, 2015, Sala Multi usos do CIC
Foils: Selected
Topics in Unification Theory: Antiunification
Access control and obligations in the category-based metamodel: a
rewriting semantics
Maribel Fernández (King's College London)
10:00-12:00, Thursday, March 26 2015, Auditório do MAT
Duodécimo Seminário Informal(, mas Formal!) do
Grupo de Teoria da Computação
organizado por Daniele Nantes, como parte do VII
Workshop de Matemática Aplicada 2015
Data: 5-6 Fev 2015
Locais: Auditório Departamento de Matemática, UnB
Programa
Foils of the talks available:
"Formal Models for
Security and Authenticity" by Mario Benevides
"She does me good - How Logic Doesn't Let You Down" by
João Marcos
"Declarative Programming
with Sequence and Context Variables" by Besik Dundua
"Formalizando
unificação nominal" by Washington L. Ribeiro
"Succinct Data Structures
for All" by Daniel Saad Nogueira Nunes
"Computação
com finitude não-padrão" by Edward Hermann
Haeusler
"Propositional
Equality, Identity Types and Homotopies" (external link)
Ruy de Queiroz
"A unified procedure for
provability and counter-model generation in Minimal implicational
logic" by Jefferson Santos
"Complexidade da
distância de translocação para genomas sem
sinal" by Lucas Angelo Silveira
A Proof Theoretic Study of Soft Concurrent Constraint Programming
Carlos
Olarte (UFRN and U. Javeriana - Cali)
15:00-16:00, Friday, April 25 2014, Sala Multi usos do CIC
Abstract:
Concurrent Constraint Programming (CCP) is a simple and powerful model
for concurrency where agents interact by telling and asking
constraints. Since their inception, CCP-languages have been designed
for having a strong connection to logic. In fact, the underlying
constraint system can be built from a suitable fragment of
intuitionistic (linear) logic --ILL-- and processes can be interpreted
as formulas in ILL. Constraints as ILL formulas fail to represent
accurately situations where "preferences" (called soft constraints)
such as probabilities, uncertainty or fuzziness are present. In order
to circumvent this problem, c-semirings have been proposed as
algebraic structures for defining constraint systems where agents are
allowed to tell and ask soft constraints. Nevertheless, in this case,
the tight connection to logic and proof theory is lost. In this work,
we give a proof theoretical interpretation to soft constraints: they
can be defined as formulas in a suitable fragment of ILL with
subexponentials (SELL) where subexponentials, ordered in a c-semiring
structure, are interpreted as preferences. We hence achieve two goals:
(1) obtain a CCP language where agents can tell and ask soft
constraints and (2) prove that the language in (1) has a strong
connection with logic. Hence we keep a declarative reading of
processes as formulas while providing a logical framework for soft-CCP
based systems. An interesting side effect of (1) is that one is also
able to handle probabilities (and other modalities) in SELL, by
restricting the use of the promotion rule for non-idempotent
c-semirings.This finer way of controlling subexponentials allows for
considering more interesting spaces and restrictions, and it opens the
possibility of specifying more challenging computational systems.
Escola de Verão do MAT/UnB 2014 - Palestras em Teoria da
Computação - Organização
GTC/UnB
Data: 20-21 Feb 2014
Local: Auditório Departamento de Matemática, UnB
Programa
Décimo primeiro Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
Data: 28-29 Nov 2013
Locais: Auditório Departamento de Matemática (28th)
Sala Multiuso Dep. C. Computação (29th) e, UnB
Programa
Witheboard images and foils of the talks available:
"A type system for
concurrent programs, that enforces data-race freedom" by Thibaut
Balabonski (Mezzo project)
"A Nonstandard
Standardisation Theorem" by Eduardo Bonelli
"A Framework for Linear
Authorization Logics" by Vivek Nigam
"On the average number of
reversals needed to sort signed permutations" by Thaynara A. Lima
"Automation of
Termination: Abstracting Calling Contexts through Matrix-Weighted
Graphs" by Andréia B. Avelar
"Computational Logic for
Computer Science" by Mauricio Ayala-Rincón and Flávio L.C. de Moura
Mini-curso: Nominal Rewriting
Maribel
Fernández (King's College London and École Normale Supérieure)
10:00-12:00, Friday, August 16 2013, Auditório do MAT
10:00-12:00, Wedsnesday, September 4 2013, Sala Multi usos do CIC
Abstract:
Nominal logic is a generalisation of first-order logic that allows
us to deal with syntax involving binding operators in an elegant and
practical way. Nominal systems maintain a strict distinction between
atoms (variables that may be bound by a special abstraction operation)
and meta-variables (or just variables) which cannot be bound, giving
the framework a pronounced first-order character since substitution is
not capture-avoiding.
In nominal syntax, bound entities are explicitly named (rather
than using a nameless syntax such as de Bruijn indices), yet we
get a formalism that respects alpha-equivalence and can be directly
implemented. Nominal unification is decidable (unlike higher-order
unification), and efficient unification algorithms are available.
Nominal rewriting can be seen as a form of higher-order rewriting
with a first-order syntax and built-in alpha-equivalence.
In these lectures, we will introduce the nominal approach to the
specification of systems with binding operators, and we will
show how good properties of first-order rewriting are inherited
by the nominal rewriting framework. We will describe an efficient
matching algorithm that has been used to implement a nominal
rewriting tool.
A combinatorial argument for termination properties
Daniel Lima Ventura (II/UFG) April 23, 2013:
14:00-16:00, Sala Multiusos CIC/UnB
Foils
Abstract:
Nonidempotent intersection type systems have
been proposed in order to give an upper bound
in computing (head) normal forms in the lambda
calculus. In this talk we give a simple syntactic
argument about the typings in order to prove
termination properties in such systems.
Definability and full abstraction problems for lambda calculi
Antonio Bucciarelli (Preuves, Programmes et
Systèmes da Université Paris Diderot (U. Paris 7) ) April 16, 2013:
14:00-16:00, Sala Multiusos CIC/UnB
Foils
Abstract:
Full Abstraction problems are about the relation
between the operational and the denotational semantics of a given
calculus/programming language. A key property for
proving full abstraction is the definability of the (finite)
elements of the denotational model. In this talk, I will survey some
classic
results on the full abstraction problem for the language PCF
of Scott and Plotkin, and then present some recent work on
full abstraction for the resource lambda calculus of Ehrhard's et al.
From Scilab To High Performance Embedded Multicore Systems – The ALMA Approach
Timo Strip (Institut fuer Technik der Informationsverarbeitung (ITIV), Karlsruher Institut fuer Technologie - KIT, Germany) March 12, 2013:
14:00-16:00, Sala Multiusos CIC/UnB
Abstract:
The mapping process of high performance embedded applications to
today’s multiprocessor system on chip devices suffers from a complex
toolchain and programming process. The problem here is the expression
of parallelism with a pure imperative programming language which is
commonly C. This traditional approach limits the mapping, partitioning
and the generation of optimized parallel code, and consequently the
achievable performance and power consumption of applications from
different domains. The Architecture oriented paraLlelization for high
performance embedded Multicore systems using scilAb (ALMA) European
project aims to bridge these hurdles through the introduction and
exploitation of a Scilab-based toolchain which enables the efﬁcient
mapping of applications on multiprocessor platforms from high level of
abstraction. This holistic solution of the toolchain allows the
complexity of both the application and the architecture to be hidden,
which leads to a better acceptance, reduced development cost, and
shorter timeto-market. Driven by the technology restrictions in chip
design, the end of exponential growth of clock speeds, and an
unavoidable increasing request of computing performance, ALMA is a
fundamental step forward in the necessary introduction of novel
computing paradigms and methodologies.
FlexTiles - Self adaptive heterogeneous manycore based on Flexible Tiles
Gabriel Marchesan Almeida (Institut fuer Technik der Informationsverarbeitung (ITIV), Karlsruher Institut fuer Technologie - KIT, Germany) March 11, 2013:
10:00-12:00, Sala Multiusos CIC/UnB
Abstract:
A major challenge in computing is to leverage multi-core
technology to develop energy-efficient high performance systems. This
is critical for embedded systems with a very limited energy budget as
well as for supercomputers in terms of sustainability. Moreover the
efficient programming of multi-core architectures, as we move towards
manycores with more than a thousand cores predicted by 2020, remains
an unresolved issue. The FlexTiles project will define and develop an
energy-efficient yet programmable heterogeneous manycore platform with
self-adaptive capabilities. A virtualisation layer on top of a kernel
hides the heterogeneity and the complexity of the manycore and
fine-tunes the mapping of an application at runtime. The
virtualisation layer provides self-adaptation capabilities by
dynamically relocation of application tasks to software on the
manycore or to hardware on the reconfigurable area. This
self-adaptation is used to optimise load balancing, power consumption,
hot spots and resilience to faulty modules. The reconfigurable
technology is based on a virtual bitstream that allows dynamic
relocation of accelerators just as software based on virtual binary
code allows task relocation. This flexibility allows the use of fault
mitigation schemes, a crucial issue for future manycores. During the
execution of the application, the runtime binding is done to match the
configuration defined by the virtualisation layer. It adapts the
location of the code, the storage and the communication paths on the
fly. Site: http://www.flextiles.eu
Décimo Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
Data: 28 Fev - 1 Mar 2013
Locais: Sala Multiuso Dep. C. Computação (28) e Sala "A" Departamento de Matemática (1ro), UnB
Programa
Lógica de Descrição Intuicionista e Fromalização de Legislação
Edward Hermann Haeusler (Pontificia Universidade Catolica de Rio de Janeiro) Novembro 29, 2012:
10:00-11:00, Auditório do Departamento de Mateática/UnB
Abstract:
lógica de descrição tem sido usada com frequência na representação de conhecimento.
O termo "Ontologia" é usado, por vezes, para denotar o conhecimento representado em um
domínio específico. Lógicas de descrição são bastante utilizadas na construção de ontologias.
No caso específico de representação do domínio Legal, a lógica de descrição usual não é
adequada. Nesta palestra, mostra-se como uma versão Intuicionista da Lógica de Descrição (iALC)
é mais adequada na formalização da área Jurídica. Apresenta-se iALC, e um caso de conflito de
leis no espaço, escopo do Direito Privado Internacional, apresentado em iALC, com uma
ontologia jurídica associada.
Curry-Howard for Justification Logic
Eduardo Bonelli (CONICET e Universidad Nacional de Quilmes) October 24, 2012
14:30-16:00, Auditório do MAT
Foils
Abstract: Justification Logic (JL) is a refinement of modal logic that has recently
been proposed for explaining well-known paradoxes arising in the formalization
of Epistemic Logic. Assertions of knowledge and belief are accompanied by
justifications: the formula [t]A states that t is “reason” for knowing/believing A.
After an overview of JL we shall focus on devising computational interpretations
for it via the Curry-de Bruijn-Howard isomorphism. Two avenues are explored:
certifying mobile computation and history-aware computation.
Talk: A framework to specify access control policies in distributed environments
Maribel Fernández (King's College London) Friday, September 28, 2012
10:00-12:00, Auditório do MAT
Abstract: In this talk, we present a meta-model for access control that
takes into account the requirements of distributed environments, where
resources and access control policies may be distributed across several
sites. This framework extends the ideas underlying Barker's
category-based meta-model. We use term rewriting to give an operational
semantics to the distributed meta-model, and then show how various
distributed access control models (e.g., MAC, DAC, RBAC, Bell-Lapadula)
can be derived as instances of the meta model. Based on work done
jointly with Clara Bertolissi.
Mini-curso: Optimal reductions
Thibaut Balabonski (Université Paris Diderot) September 10-14, 2012
10:00-12:00, Auditório do CIC, Módulo 18
Abstract: In functional programs the order of evaluation need not be fully specified by the programmer, which gives to compilers some freedom in scheduling computations. However, the many possibilities may allow substantial variations in the execution time of a program. So-called “optimal reductions” are rewriting sequences that produce the result of a program using a minimal number of steps, and characterize lower bounds on the evaluation of programs.
This mini-course is a broad introduction to optimality and to efficient reduction strate- gies in the lambda-calculus and in rewriting theory, ranging from decidability issues to implementation techniques. Some highlights will be:
• the impossibility of defining an effective optimal reduction strategy for the usual lambda-calculus,
• the replacement of terms by graphs to circumvent this problem, • the decoration of terms with labels to represent graphs without ever manipulating
them directly,
• the transformation of programs by lambda-lifting to reduce a higher-order problem to a much simpler first-order problem,
• the relative optimality of a reduction strategy based on lazy evaluation and on mem- orization of intermediaite results in the style of Haskell.
Problemas Decidíveis e Problemas Indecidíveis: O Legado de Alan Turing
Ruy de Queiroz (Centro de Informática, UFPE) June 21, 2012
Thursday 21 June, 14:30-16:00, Auditório do MAT
Abstract: Alan Turing (1912-1954), matemático, lógico, criptoanalista e cientista da computação britânico, foi fundamental no desenvolvimento da ciência da computação e proporcionou uma formalização do conceito de algoritmo e computação através do modelo matemático idealizado da "máquina de Turing". Tendo desempenhado importante papel na quebra do código da máquina ENIGMA utilizada pelo exército alemão na Segunda Guerra, passou de herói de guerra a um fora-da-lei sujeito a tratamento quimico-hormonal forçado devido a sua homossexualidade. Em homenagem ao centenário de seu nascimento, a intenção aqui é fazer uma reflexão sobre o legado desse que foi, ao mesmo tempo, herói nacional e uma ameaça ao estado britânico: de fundamental importância na consolidação da ciência da computação, da noção de máquina universal, assim como da teoria da decidibilidade de problemas matemáticos, Turing abriu caminho para a demonstração de que certos problemas da Matemática são indecidíveis, a exemplo do décimo problema de Hilbert. Alguns subprodutos de sua investigação teórica, tais como o computador de propósito geral e a noção de inteligência artificial, serviram de base para os que muitos chamam de "Quarta Revolução Tecnológica - A Revolução da Informação".
Mini-curso: Normalisation for Dynamic Pattern Calculi
Eduardo Bonelli (CONICET e Universidad Nacional de Quilmes) May 22-23, 2012
Tuesday 22 May, 16:00-18:00, Auditório do CIC, Módulo 18
Wedsnesday 23rd May, 10:00-12:00, Auditório do MAT
Foils of the mini-course:
Foils
Abstract: The Pure Pattern Calculus (PPC) extends the Lambda Calculus, as well as the family of algebraic pattern calculi, with first-class patterns i.e. patterns can be passed as arguments, evaluated and returned as results. The notion of *matching failure* of PPC not only provides a mechanism to define functions by pattern matching on cases but also supplies PPC with parallel-or-like, non-sequential behaviour. Therefore, devising normalising strategies for PPC to obtain well-behaved implementations turns out to be challenging. This talk focuses on normalising reduction strategies for PPC. We define a (multistep) strategy and show that it is normalising. The strategy generalises the leftmost-outermost strategy for Lambda Calculus and is strictly finer than parallel-outermost. The normalisation proof is based on the notion of *necessary set of redexes*, a generalisation of the notion of needed redex encompassing non-sequential reduction systems.
Work developed in collaboration with Delia Kesner, Carlos Lombardi and Alejandro Ríos.
Mini-curso: Lambda-calculus, Linear Logic and Explicit Substitutions
Beniamino Accattoli (INRIA team at LIX Paris, Françai) March 19-22, 2012
10:00-12:00, Auditório do CIC, Módulo 18
Foils of the mini-course and talk:
Linear Logic,
Proof Nets,
Rewriting,
Variations,
Palestra: The Permutative Lambda-Calculus
Beniamino Accattoli (INRIA team at LIX Paris, Françai) March 23, 2012
10:00-12:00, Auditório da Matemática
Foils of the talk: foils
Nono Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
Data: 8-9/Dezembro/2011
Local: Auditório Departamento de Matemática, UnB
Programa
Construction of Reduction Rings and Effective Ideal Operations
Klaus Madlener ( Fachbereich Informatik, Universität Kaiserslautern, Germany) November 8, 2011:
16:00-18:00, Auditório da Matemática/UnB
Abstract:
Buchberger's algorithm and more generally the notion of Gröbner Bases or
Standard Bases for ideals turned out to be of great value in many applications
where rings play a role. Since it's introduction several notions of Gröbner
Bases have been used depending on the intended application and the ring type.
In this talk we compare these notions in the abstract setting of reduction
rings and their constructions.
In which sense is Natural Deduction Natural?
Edward Hermann Haeusler (Pontificia Universidade Catolica de Rio de Janeiro) Novembro 4, 2011:
14:00-16:00, Auditório do Departamento de Mateática/UnB
Automated Specification Analysis Using an Interactive Theorem Prover
Pete Manolios (Northeastern University, Boston, USA) August 26, 2011:
14:00-16:00, Auditório do CIC/UnB - Palestra inaugural PPGInfo
Abstract:
Many formal methods techniques have been developed that help designers
build complex, dependable systems. At one extreme we have interactive
theorem proving, which places few restrictions on the kinds of systems
and properties that can be verified, but which requires well trained
professionals with a deep understanding of logic and proof. At the
other extreme, we have methods that ﬁnd certain classes of errors in a
fully automated way, but which place severe restrictions on the kinds
of systems and properties they can analyze.
I will show that it is possible to have the best of both worlds. It is
possible to have a powerful, expressive modeling language with a
powerful deductive engine that can be used to interactively prove
theorems and that can be used to automatically generate
counterexamples. The crux of our method is the synergistic integration
of testing with the deductive reasoning engine of the ACL2 Sedan
interactive theorem prover. We have implemented and experimentally
validated the method in the ACL2 Sedan, an open source Eclipse
plug-in that provides a modern integrated development environment
designed to bring computer-aided reasoning to the masses. ACL2s has
been used in several sections of a required freshman course at
Northeastern University to teach
several hundred undergraduate students how to reason about programs.
Aiming at the Natural Equilibrium of Planet Earth Requires to Reinvent Computing
Reiner Hartenstein (Universität Kaiserslautern and KIT, Germany) Mai 20, 2011:
14:00-16:00, Auditório do CIC/UnB - Palestra inaugural PPGInfo
Abstract:
Maintaining the natural equilibrium of the planet earth requires increasing compute capacity also to optimize all key issues given by the impact of the growing population of human beings and their activities. Already now the carbon footprint of only the internet is higher than that of the worldwide air traffic. Under the growing oil price at declining production the rapidly growing energy consumption in all areas of computing will become unaffordable, probably within less than a decade.
Growing core counts of manycore architectures are racing ahead of programming paradigms. Most applications had originally been written for a single processor and more than 50% of the applications do not scale beyond eight processor cores. The programmer population qualified for re-writing does not yet exist.
Programming research has stalled and the parallel programming wall forces us to reshape the fundamental nature of system design, programming methods and system usage. However, the evolutionary path is not addressing the key issues. Extrapolations from current methods and practices are simply inadequate. Hetero systems including reconfigurable computing promise to reduce the energy consumption of computing by at least an order of magnitude. However, for a successful transition we have to reinvent computing.
Reconfiguration Techniques for Self-X Power and Performance Management in the context of organic computing
Christian Schuck (Institut fuer Technik der Informationsverarbeitung (ITIV), Karlsruher Institut fuer Technologie - KIT, Germany) Marz 9, 2011:
16:00-18:00, LAB-GRACO/UnB
Abstract:
Module-based partial reconfiguration of FPGAs offers
great possibilities for runtime flexibility. It enables
hardware tasks to swap in and out the design without
interruption of the entire system. In this context the
techniques of module relocation and the 2-dimensional
reconfiguration have been successfully applied in order to
reduce the storage requirement for partial bit-streams and
to shorten the reconfiguration times significantly. Besides
the adaptation on functional level, multiple clock domains
and dynamic frequency scaling are key techniques to
achieve an adaptation on power and performance level as
well. However, current approaches of module relocation
provide no real support for designs with multiple clock domains.
Further online monitoring techniques are necessary to enable the system to
Self-adapt, according to environmental and internal changes.
KAHRISMA: A Novel Hypermorphic Reconfigurable-Instruction-Set Multi-grained-Array Architecture
Timo Strip (Institut fuer Technik der Informationsverarbeitung (ITIV), Karlsruher Institut fuer Technologie - KIT, Germany) Marz 9, 2011:
14:00-16:00, LAB-GRACO/UnB
Abstract:
Due to the diverse processing behavior and unpredictable nature of the next generation applications future embedded devices may no longer perform efficiently when following current trends, e.g. when a design is tailor made for a specific scenario or application domain. We believe that crucial design decisions can no longer be fixed/determined at design time. This begets the demand for an innovative processor architecture reacting flexibly to the run-time scenarios. Therefore we are researching a novel multi-grained reconfigurable hardware architecture, tightly integrating coarse and fine-grained reconfigurable fabrics extended by the capability to handle different Instruction Set Architectures (ISAs) in parallel. A flexible, retargetable software framework is needed to make use of the novel features of the proposed architecture. The framework is suitable for mixed-ISA application development as well as design space exploration (DSE). Therefore, we developed a novel mixed-ISA, compiler- and simulator-centric, behavioral architecture description language (ADL). The ADL provides the necessary flexibility to describe multiple ISAs for the software framework. The individual framework tools -- the compiler, binary utilities, and instruction set simulator (ISS) -- are generated from an ADL description. To realize the complex compiler inside the framework, we extended the LLVM compiler infrastructure by a mixed-ISA retargetable code generator (compiler back-end).
Oitavo Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
Data: 3-4/Fevereiro/2011
Local: Auditório Departamento de Matemática, UnB
Programa
17^{th} Workshop on Logic, Language, Information and Computation - WoLLIC 2010
Jul 6th - 9th, 2010
Sétimo Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
Data: 12-13/Novembro/2009
Local: Auditório Departamento de Matemática, UnB
Programa
Federated Conference on Rewriting, Deduction and Programming RDP 2009
Data: 22 de Junho a 03 de Julho de 2009
Local: Departamento de Matemática e FINATEC
Sexto Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
Data: 30 e 31 de outubro/2008
Local: Anfiteatro 2 do Departamento de Computação
Our Computing Habits Unaffordable soon, and: a Climate Disaster
Reiner Hartenstein (Universität Kaiserslautern and KIT, Germany) September 25, 2008:
16:00-18:00, Auditório da Reitoria / UnB
PDF of the talk
Third Workshop on Logical and Semantic Frameworks with Applications
Organised in Salvador, 26-27 August, 2008. LSFA'08 Program and Papers.
Os Desafios da Busca Distribuída na Web.
Quinta-feira Abril 10, 2008, 14:00-15:00, Auditorium MAT/UnB
Ricardo Baeza-Yates, VP of Research Yahoo! Research
Departamento de Ciencia de la Computación, Universidad de Chile
Santiago de Chile.
Quinto Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
Dias 6 e 7 de dezembro/2007
Second Workshpo on Logical and Semantic Frameworks with Applications
Organised in Ouro Preto, 27-28 August, 2007. LSFA'07 Program and Foils.
The MathLang Framework for Computerizing and Checking Mathematics.
Fairouz Kamareddine (Heriot-Watt University, Edinburgh, U.K.).
August 24, 2007. 10:00-12:00, Auditório MAT/UnB
Slides of Fairouz' talk in PDF, also available at LSFA'07 Program.
Escola de Verao 2007 MAT/UnB, Semana de Teoria da Computação
05-09 Fevereiro, 2007
Teoria da Computação: tipos e provas matemáticas.
(Indicada para todos os alunos do verão)
Mauricio Ayala-Rincón (Departamento de Matemática, UnB)
February 9, 2007. 16:30-18:00:
PDF da palestra
Mini-course on Rewriting, Explicit Substitutions and Normalisation.
Eduardo Bonelli (
Laboratorio de Investigación y Formación en Informática Avanzada, Facultad de Informática, Universidad de La Plata)
February 7, 2007. 09:00-10:30, Talk 1: Needed Strategies
Slides (PDF)
February 7, 2007. 11:00-12:30, Talk 2: Explicit Substitutions
Slides (PDF)
February 8, 2007. 16:30-18:00, Talk 3: Rewriting, Lambda Calculus (Indicada para todos os alunos do verão)
Slides (PDF)
Abstract: In this mini-course we study an extension of the theory of needed
normalisation to non-orthogonal term rewrite systems and its application to calculi with
explicit substitutions. No knowledge of rewriting is assumed.
Quarto Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
07-08 Dezembro, 2006
MathLang: a Framework for Computerising Mathematics.
Fairouz Kamareddine (Heriot-Watt University, Edinburgh, U.K.).
September 14, 2006. 14:30-16:15, Auditório MAT/UnB
Slides of the talk in PDF.
Abstract:
We report on the findings of the MathLang project which started in 2001 by Fairouz Kamareddine and Joe Wells and which includes Manuel Maarek and Krzyztof Retel
Frege was frustrated by the use of natural language to describe mathematics. In the preface to his Begriffsschrift he says:
"I found the inadequacy of language to be an obstacle; no matter how unwieldy the expressions I was ready to accept, I was less and less able, as the relations became more and more complex, to attain the precision that my purpose required."
Frege therefore presented in his Begriffsschrift, the first extensive formalisation of logic giving logical concepts via symbols rather than natural language. Frege developed things further in his Grundlagen and Grundgesetze der Arithmetik which could handle elementary arithmetic, set theory, logic, and quantification. In his Grundlagen der Arithmetik, Frege argued that mathematics can be seen as a branch of logic. In his Grundgesetze der Arithmetik, he described the elementary parts of arithmetic within an extension of the logical framework of Begriffsschrift. Frege's tradition was followed by many others: (Russell, Whitehead, Ackermann, Hilbert, etc.). Russell discovered a paradox in Frege's work and proposed type theory as a remedy. Advances were also made in set theory, category theory, etc., each being advocated as a better foundation for mathematics. But, none of the logics proposed satisfies all the needs of mathematicians. In particular, they do not have linguistic categories and are not a satisfactory communication medium. Moreover:
Explaining Concepts in Compositional Type-Based Program Analysis:
Principality, Intersection Types, Expansion, etc.
Joe Wells (Heriot-Watt University, Edinburgh, U.K.).
September 14, 2006. 16:30-18:00, Auditório MAT/UnB
Slides of the talk in PDF.
Abstract:
A static program analysis predicts program behavior without actually
running the program. An analysis is compositional when the
analysis result for each program part depends only on the results
for the immediate sub-parts, which can therefore be analyzed in
isolation (using zero information about their context) and in any
order. Doing analysis compositionally is challenging in all
approaches to program analysis, and in the case of type-based
analysis tends to conflict with the ∀ ("for all") quantifiers most
commonly used to gain type polymorphism which is needed for
programming flexibility.
The starting point for making analysis compositional is the concept
of principal typings (not to be confused with the much weaker
notion of principal types often mentioned in connection with
ML-like languages and the Hindley/Milner type system). An analysis
result (e.g., a typing in some type system) for a program fragment
is principal for that fragment when it is stronger than all other
results for the same fragment. Without principal typings, an
analysis algorithm must either be incomplete, be non-compositional
(for example, Milner's algorithm W used for ML-like languages is
non-compositional), or use intermediate results outside of the
analysis system.
Obtaining principal typings requires using types that more closely
correspond to actual program evaluation. As an example, in the case
of the λ-calculus, intersection types correspond to the multiple
uses by a function of its parameter and the operation of expansion
on typings corresponds to the duplication (or discarding) of the
actual arguments of functions. In comparison, recent work
developing principal typings for Java-like languages has needed
novel kinds of type assumptions that correspond to object-oriented
operations like method dispatch.
This talk aims to explain and clarify in as simple a way as possible
what the above-mentioned concepts are and how they are related, and
also explain other related concepts (e.g., the rank of types,
polyvariant data flow analysis, incremental reanalysis, etc.).
A Simple Relational Correctness Theorem for General Recursive Programs.
Jaime Alejandro Bohórquez (Centro de Estudios en Ingeniería de Software, Escuela Colombiana de Ingeniería)
Mai 2, 2006. 09:00-10:30, Auditório MAT/UnB
Slides of the talk in PDF.
Abstract: we have a correctness theorem for recursive programs analogous in simplicity to
Floyd and Dijkstra's Main Repetition (or Invariance) theorem for the
correctness of iterative programs.
Based on Hoare and Jifeng's relational semantics we propose, by considering the
structure of its code and specification, "regularity conditions" on the
predicate transformer associated to the fixed-point equation of a general (non
deterministic) recursive program to prove it correct by induction on a well
founded ordering of a covering of the domain of its corresponding input-output
relation. All fixed point solutions associated to a predicate transformer
satisfying these regularity conditions coincide when restricted to the domain
of its least fixed point solution. We find these conditions non unduly
restrictive, since continuous operators defining deterministic programs as
their corresponding least fixed-point solutions must fulfill them.
Real Number Calculations and Interval Analysis in PVS.
César Muñoz (Formal Methods Group, National Institute of Aerospace and NASA Langley Research Center)
April 19, 2006. 14:30-15:30, Auditório MAT/UnB
Slides of the talk in PDF.
Abstract: Type theory was invented at the begining of the XX century with the purpose of eliminating the paradoxes which come from the application of the function to itself. The Lambda Calculus was developed (by Church) around 1930 as a theory of functions. In 1940, Church added types to his Lambda Calculus. This types were simple, which means they were never constructed using a binder (like Lambda). So, we have terms like $\lambda_{x:T}.B$ (which are constructed with the binder Lambda), but there are no binders which we can use to construct types. Despite the influence of Church's Lambda calculus, its limitation led to the creation of many typed theories in the second half of the XX century. In this calculi, the types are constructed with binders. In most of these calculi we find two binders: the $\lambda$ (to construct terms) and the $\Pi$ (or $\forall$, to construct types). These two binders allow us to distinguish functions (which we construct with $\lambda$) and types (which we construct with $\Pi$). Moreover, in these calculi we allow $\beta$-reduction, but not $\Pi$-reduction. In other words, in these calculi we have the rule:
Abstract: wouldn't it be nice to be able to conveniently use ordinary real number
expressions within proof assistants? In this talk, we outline how this
can be done within a theorem proving framework. First, we formally
establish upper and lower bounds for trigonometric and transcendental
functions. Then, based on these bounds, we develop a rational interval
arithmetic where real number calculations can be performed in an
algebraic setting. This pragmatic approach has been implemented as a set
of strategies in PVS. The strategies provide a safe and convenient way
to perform explicit calculations over real numbers in formal proofs.
Pure Pattern Calculus.
Delia Kesner (Laboratoire Preuves Programmes et Systèmes
Université Paris 7 - Denis Diderot
)
(joint work with Barry Jay)
April 19, 2006. 16:00-17:00, Auditório MAT/UnB
Abstract: The pure pattern calculus generalises the pure lambda-calculus by
basing computation on pattern-matching instead of
beta-reduction. The simplicity and power of the calculus derive from
allowing any term to be a pattern. As well as supporting a uniform
approach to functions, it supports a uniform approach to data
structures which underpins two new forms of polymorphism. Path
polymorphism supports searches or queries along all paths through an
arbitrary data structure. Pattern polymorphism supports the
dynamic creation and evaluation of patterns, so that queries can be
customised in reaction to new information about the structures to be
encountered.
As the variables used in matching can now be eliminated by reduction
it is necessary to separate them from the binding variables used to
control scope. Then standard techniques suffice to ensure that
reduction progresses and to establish confluence of reduction.
Mini-course on logic and rewriting: Extending the Explicit Substitution Paradigm.
Delia Kesner (Laboratoire Preuves Programmes et Systèmes
Université Paris 7 - Denis Diderot)
(joint work with Stephane Lengrand)
April 18, 2006. 14:30-16:00+16:30-18:00, Auditório MAT/UnB
Delia's "enseignement" page with material of the talk.
Abstract: We present a simple term language with explicit operators for
erasure, duplication and substitution enjoying a sound and complete
correspondence with the intuitionistic fragment of Linear Logic's
Proof Nets. We establish the good
operational behaviour of the language by means of some
fundamental properties such as confluence, preservation of
strong normalisation, strong normalisation of well-typed terms
and step by step simulation. This formalism is the
first term calculus with explicit substitutions having full composition and
preserving strong normalisation.
The typed Lambda Calculus with a Single Binder.
Fairouz Kamareddine (Heriot-Watt University, Edinburgh, U.K.).
April 21, 2006. 14:30-16:15, Auditório MAT/UnB
Slides of the talk in PDF. See also the related paper Typed lambda calculi with unified binders, in J. Funct. Programming 15(5):771-796, 2005.
Abstract: Type theory was invented at the begining of the XX century with the purpose of eliminating the paradoxes which come from the application of the function to itself. The Lambda Calculus was developed (by Church) around 1930 as a theory of functions. In 1940, Church added types to his Lambda Calculus. This types were simple, which means they were never constructed using a binder (like Lambda). So, we have terms like $\lambda_{x:T}.B$ (which are constructed with the binder Lambda), but there are no binders which we can use to construct types. Despite the influence of Church's Lambda calculus, its limitation led to the creation of many typed theories in the second half of the XX century. In this calculi, the types are constructed with binders. In most of these calculi we find two binders: the $\lambda$ (to construct terms) and the $\Pi$ (or $\forall$, to construct types). These two binders allow us to distinguish functions (which we construct with $\lambda$) and types (which we construct with $\Pi$). Moreover, in these calculi we allow $\beta$-reduction, but not $\Pi$-reduction. In other words, in these calculi we have the rule:
$(\lambda_{x:A}.B)C \rightarrow B[x:=C]$
But not the rule:
$(\Pi_{x:A}.B)C \rightarrow B[x:=C]$
In particular, when $b$ has the type $B$, we give to $(\lambda_{x:A}.b) C$ the type $B[x:=C]$ instead of $(\Pi_{x:A}.B) C$. There are some powerfull extensions of type theory which give $\Pi$ the same behaviour as $\lambda$ (for example, in Automath, and in the programming language Henk of Simon Peyton Jones, etc.). This leads us to ask the question: Why distinguish between $\lambda$ and $\Pi$ when systems like Automath showed us that it is more advantageous to treat types exactly like terms? In this talk, I describe a system where the two binders are identified and show that the system has all the properties that we expect from a type system except for unicity of types, but I also show that the loss of unicity of types is not serious because there is an isomorphism between typing using two binders and typing using a single one. Moreover, I show that all the different types of the same term follow the same pattern.
Escola de Verao 2006 MAT/UnB, Semana de Teoria da Computação
02-03 Fevereiro, 2006
Terceiro Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
01-02 Dezembro, 2005
Sistemas Multi-Agentes e Jogos.
Edward Hermann Haeusler (Departamento de Informática, PUC-RIO)
September 26, 2005:
Pdf da palestra
Resolvedores modernos de SAT.
Marcelo Finger (Departamento de Ciência da Computação, IME-USP)
September 2, 2005:
Pdf da palestra
Desenvolvimento Orientado a Linguagens e Lógica de Reescrita
Christiano Braga (Departamento de Ciência da Computação, UFF)
10:00-12:00, Julho 5, 2005:
1, 2 PDFs da palestra
Matching via Explicit Substitutions
Flávio Leonardo Cavalcanti de Moura (Departamento de Matemática, UnB)
14:00-16:00, June 1, 2005:
PDF da palestra
Comparing Huet's Unification Procedure and Higher Order Unification via Explicit Substitutions Calculi.
Flávio Leonardo Cavalcanti de Moura (Departamento de Matemática, UnB)
14:00-16:00, April 27, 2005:
PDF da palestra
Demonstrações, Tipos e o Cálculo de Inferência do Assistente de Provas PVS.
André Luiz Galdino (Departamento de Matemática, UnB)
10:00-12:00, April 27, 2005:
Postscript, PDF da palestra
Tipos, provas e o problema de existência de habitantes.
Mauricio Ayala-Rincón (Departamento de Matemática, UnB)
January 17, 2005:
Postscript, PDF da palestra
Complexidade Computacional e Jogos.
Edward Hermann Haeusler (Departamento de Informática, PUC-RIO)
January 14, 2005:
Powerpoint da palestra
Ordenação Ótima.
PDF
José de Siqueira (UFMG). Nov. 12, 2004
Segundo Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
28-29 Outubro, 2004
Web Query Mining.
Saturday October 23, 2004, 10:00-12:00, Auditorium MAT/UnB
Ricardo Baeza-Yates, Director Center for Web Research (CWR)
Departamento de Ciencia de la Computación, Universidad de Chile
Santiago de Chile.
Abstract:
User queries in search engines and Websites give valuable information
on the interests of people. In addition, clicks after queries relate
those interests to actual content. Even queries without answers
imply important missing synonims or content. In this talk we show
several examples and the associated algorithms on how to use this
information to improve the performance of search engines, to
recommend better queries, and to improve the information scent of the
content of a Website.
Palestra Similitud de Sequencias, WOB 2004, PDF
Partial Reconfigurable Systems for automotive applications.
September 16, 2004, 14:30-16:00, Auditorium Eng. Mecânica/UnB
Foils of the Talk.
Development of Software and Designflow for Xilinx FPGAs.
September 17, 2004, 10:00-12:00, Auditorium Eng. Mecânica/UnB
Foils of the Talk.
Michael Hüebner huebner@itiv.uni-karlsruhe.de (Institut für Technik der Informationsverarbeitung - ITIV , Universität Karlsruhe (TH), Germany)
Descritividade em Sistemas Formais com Respeito ao Problema P=^{?}NP
Claus Akira H. Matsushigue (IME/USP, São Paulo & IGCE/UNESP, Rio Claro) February 12, 2004:
10:00-11:00, Anphiteater MAT/UnB
postscript of the talk
More recent developments in Reconfigurable Computing
Reiner Hartenstein (Universität Kaiserslautern, Germany) November 14, 2003:
16:30-18:00, Anphiteater MAT/UnB
Power point of the talk
Primeiro Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
30-31 Outubro, 2003
Teoria de Categorias e Computação.
Edward Hermann Haeusler (Departamento de Informática, PUC-RIO)
February 7, 2003:
Powerpoint da palestra
Mini-course on Reconfigurable Systems.
Reiner Hartenstein (Universität Kaiserslautern, Germany) November 11-22, 2002:
First section. 13.11, Wednesday, 16:00-18:00;
Second and Third sections. 14.11, Thursday, 08:00-10:00, 16:00-18:00;
Fourth and fifth sections. 21.11, Thursday, 08:00-10:00, 16:00-18:00,
Anphiteater CIC/UnB
Power point 1 of the talk.
Power point 2 of the talk.
Power point 3 of the talk.
Power point 4 of the talk.
Configurable Systems-on-Chip (CSoC).
Jürgen Becker (Institut für Technik der Informationsverarbeitung - ITIV, Universität Karlsruhe (TH), Germany) September 5, 2002, 16:00-18:00, Auditorium FT/UnB (local to be defined)
Abstract of the talk.
On Automating the Extraction of Programs from Proofs Using Product Types.
François Monin (IRISA, Campus de Beaulieu, Rennes, France) August 5 and 7, 2002
Talk in postscript.
Evolution of Types and Functions in the 20
Fairouz Kamareddine (Heriot-Watt University, Edinburgh, U.K.). July 22 and 29, 2002
Talk in postscript. See also the paper TYPES IN LOGIC AND MATHEMATICS BEFORE 1940, in Bull. Symbolic Logic, 8(2):185-245, 2002.
8^{th} Workshop on Logic, Language, Information and Computation - WoLLIC'2001
Jul 31 - Aug 03, 2001
Métodos Formais e Modelagem e Verificação de Sistemas Hipermídia.
Edward Hermann Haeusler (PUC-Rio). July 09, 2001
II Encontro de Matemática Aplicada e Computacional em Brasília
Seção Computação, Fev 13, 2001
Palestras por
Properties of Combinations of Rewrite Systems
Nachum Dershowitz (University of Illinois at Urbana-Champaign). Jul 27-28, 1998
Lógica e Demonstração Automática de Teoremas.
José de Siqueira (UFMG). Feb. 18-20, 1998
Temporal Reasoning in the Situation Calculus.
Leopoldo Bertossi (PUC-Chile). Feb. 20-26, 1997
Categorias em Computação.
Edward Hermann Haeusler (PUC-Rio). Feb. 03 - 05, 1997
Problemas de Otimização e Teoria da Complexidade
de Algoritmos.
Juan F. Diaz Frias (UNIVALLE, Cali, Colômbia). Jan. 24 -
28, 1997
Teoria de Modelos Finitos e Complexidade Algoritmica.
Xavier Caicedo (Universidad de Los Andes, Bogotá,
Colômbia / UNICAMP). Jun 21, 1996
Provas, Tipos e Dedução Rotulada.
Ruy de Queiroz (UFPE). Sep. 22, 1995
SEQUOIA: Um Demonstrador Automático de Teoremas além
do "Sim" e do "Não".
José de Siqueira (UFMG). Mar. 07, 1995