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&aacutye;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.
8th 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