text:
Events

TBA

### Past Events and Conferences

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.

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

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

17th 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

• 5a, 30 de outubro de 2008.
• 14:00-15:40 On Games and the PSPACE-completeness of Minimal and Intuitionistic Logic, with posterior discussion on Descriptive Complexity
Edward Hermann Haeusler, Professor do Departamento de Informática, PUC-Rio
• 15:40-16:10 Coffee-Break
• 16:10-17:00 Algoritmo de Landau-Vishkin Modificado Utilizando a Representação de RMQ de Fischer-Heun e sua Aplicação na Bioinformática
Leon Sólon, Mestrando em Informática, UnB
• 17:00-17:50 Tipos de Interseção e Substituições Explícitas
Daniel Lima Ventura, Doutorando em Matemática, UnB
• 6a, 31 de Outubro de 2008.
• 8:20-10:00 Procedimentos de Decisão para a Verificação de Software
David Déharbe, Professor do Departamento de Informática e Matemática Aplicada, UFRN
• 10:00-10:20 Coffee-Break
• 10:20-11:10 Resolução Clausal para Lógicas Modais Normais
Cláudia Nalon, Professor do Departamento de Ciência da Computação, UnB
• 11:10-12:00 Uma Formalização do Lema de Substituição em Notação de De Bruijn
Flávio L. C. de Moura, Professor do Departamento de Ciência da Computação, UnB

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

• 5a, 06 de dezembro de 2007.
• 6a, 08 de Dezembro de 2007.
• 8:20-09:10 Modelagem e Verificação de Propriedades Epistêmicas em Sistemas Multi-agentes
Mario Benevides (trabalho em conjunto com Carla Delgado)
, Instituto de Matemática/UFRJ.
• 9:10-10:00 Verificação formal de protocolos criptográficos
Rodrigo Borges Nogueira (trabalho em conjunto com Mauricio Ayala-Rincón),
Mestrando em Informática/UnB.
• 10:00-10:20 Coffee-Break
• 10:20-11:10 Post-quantum oblivious transfer protocol
Anderson Clayton Alves Nascimento,
Dep. de Engenharia Elétrica/UnB.
• 11:10-12:00 Verificação e falsificação de sistemas híbridos lineares: uma perspectiva histórica (slides)
Guilherme Albuquerque Pinto,
Dep. de Ciência da Computação/UnB.

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

• 5a, 07 de dezembro
• 08:20-09:20 Verificação de Sistemas de Tempo Real com Autômatos Temporizados: Teoria e Prática, Abstract, Slides (PDF)
Guilherme A. Pinto, Prof Ciência da Computação UnB
• 09:20-10:00 Implementação de um algoritmo espaço-eficiente para reconhecimento aproximado via arranjos de sufixos e considerações sobre a sua aplicação em dados moleculares ,
Rodrigo de Castro Miranda, Mestrando em Informática UnB
• 10:00-10:30 Coffe-Break
• 10:30-11:10 Um algoritmo de aproximação 1.5 baseado no formalismo algébrico para o problema da ordenação por transposição
Hederson P. Santos, Mestrando em Informática UnB
• 11:10-12:10 An Operational Characterization of (Lazy)-Strong Normalization, Abstract, Slides (PDF)
Elaine G. Pimentel, Prof. Departamento de Matemática, UFMG
• 6a, 08 de Dezembro
• 8:20-09:20 Unificação de Terceira ordem via Susbstituições Explícitas, Slides (PDF)
Flávio L. C. de Moura, Prof. Ciência da Computação UnB
• 9:20-10:00 Sistemas Lógicos subjacentes a Cálculos de Substituições Explícitas Tipados,
Daniel Ventura Lima, Doutorando em Matemática UnB, bolsista CNPq
• 10:00-10:30 Coffe-Break
• 10:30-11:10 Estratiégias da teoria de reescrita em PVS: considerações sobre especificação e aplicações, Slides (pdf), ARS: PVS theory for abstract rewriting systems
André Luiz Galdino, Doutorando em Matemática UnB, bolsista CNPq, Prof. UFG (Campus Catalão)
• 11:10-11:50 Especificação Formal de Protocolos Criptográficos, Slides (ppt)
Rodrigo Borges Nogueira, Mestrando em Informática UnB

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:

• *Logics make choices (types/sets/categories, predicative/impredicative, etc.). But different parts of mathematics need different choices. There is no agreed best formalism.
• *A logician's formalization of a {\sc Cml} text loses the original structure and is thus of little use to ordinary mathematicians.
• *Mathematicians can do their work without formal mathematical logic.
In the second half of the twentieth century, programming languages were being developed and this led to the creation of softwares, systems and tools to computerize and check mathematics on the computer, and to give some help and assistance to teachers, students, and users of mathematics. But, a mathematical text is structured differently from a machine-checked text proving the same facts. Making the latter involves extensive knowledge and many choices:
• *The Choice of the underlying logic.
• *The Choice of how to implement concepts (equational reasoning, induction, etc.).
• *The Choice of the formal system: a type theory (which?), a set theory (which?), etc.
• *The Choice of the proof checker: Coq, Isabelle, PVS, Mizar, etc.
Furthermore, checking mathematics on the computer has other problems:
• *An informal mathematical proof will cause headaches as it is hard to turn in one big step into a (series of) syntactic proof expressions.
• *During the checking of mathematics, the informal proof is replaced by a complete proof where every detail is spelled out. Very long expressions replace the clear mathematical text and this is useless to ordinary mathematicians.
• so, despite the enourmous work on logics for mathematics as in Frege's tradition, and computer tools and systems for implementing and checking mathematics as in the second half of the twentieth century, mathematicians remain sceptical about using logic and using computers.
This talk argues that both the logic for mathematics and the computation of mathematics have forgotten the mathematician and the language of mathematics during their development. I start from de Bruijn's mathematical vernacular which he refined almost twenty years after the begin of his Automath project (Automating Mathematics). I compare this vernacular to modern approaches for putting mathematics on the computer (e.g., OMDOC, MathML, versions of XML, etc.) and discuss how we can find a language of mathematics that is open to future developments through logic and computation.

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

• 5a, 02 de fevereiro
• 14:30-16:00 Raciocínio Aproximado Apresentação (PDF): parte 1, parte 2, parte 3
Marcelo Finger (Departamento de Ciência da Computação, IME-USP)
• 16:15-17:45 Análise Formal de Sistemas: uma abordagem baseada em linguagens Apresentação: PDF
Christiano Braga (Instituto de Computação, UFF)
• 6a, 03 de fevereiro
• 14:15-15:45 Provas como Objetos de Estudo: história, usos e abusos Apresentação: Power Point
Edward Hermann Haeusler (Departamento de Informática, PUC-RIO)
• 16:00-17:00 Computação Segura Distrubuida: Como Jogar com Trapaçeiros
Anderson Clayton Alves Nascimento, Engenharia Elétrica, UnB
• 17:00-18:00 O Problema P=?NP e provas robustas checáveis probabilisticamente
Claus Akira H. Matsushigue (Departamento de Matemática, UnB)

Terceiro Seminário Informal(, mas Formal!) do Grupo de Teoria da Computação
01-02 Dezembro, 2005

• 5a, 01 de dezembro
• 15:00-15:40 Ordenação por "Block-Interchanges" e reversões com sinais, Apresentação: PDF
Cleber Valgas Gomes Mira, Doutorando em Computação IC/UNICAMP, bolsista FAPESP
• 15:40-16:20 Formalismo Algébrico Para o Problema da Ordenação por transposições em Rearranjos de Genomas, Apresentação: power point
Hederson Pereira dos Santos, Mestrando em Informática UnB
• 16:20-16:40 Coffe-Break
• 16:40-17:40 Verificação Formal em PVS do Sistema KB2D de Resolução de Conflitos de Tráfego Aéreo, Apresentação: PDF
André Luiz Galdino, Doutorando em Matemática UnB, bolsista CNPq, Prof. UFG (Campus Catalão)
• 6a, 02 de Dezembro
• 8:20-09:20 Formas Normais para Lógicas Modais, Apresentação: PDF
Cláudia Nalon, Prof. Ciência da Computação UnB, PhD Univ. Liverpool.
• 9:20-10:20 Redução do Sujeto para Cálculos de Substituições Explícitas com Tipos Simples, Apresentação: PDF
Daniel Ventura Lima, Mestrando em Matemática UnB, bolsista CNPq
• 10:20-10:40 Coffe-Break
• 10:40-11:40 Comparação de Seqüências Biológicas em Hardware Reconfigurável, Apresentação: PDF
Jan Mendonça Corrêa, Doutorando en Engenharia Elétrica, UnB, Prof. Ciência da Computação UnB

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

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

• 5a, 28 de outubro
• 14:30-15:40 Tipando Cálculos de Substituições Explícitas, Apresentação: PDF, postscript
Mauricio Ayala-Rincón, Prof. MAT/UnB
• 15:40-16:10 Coffe-Break
• 16:10-17:20 Semântica e Tipos Dependentes do PVS e Aplicações, Apresentação: PDF
André Luiz Galdino, Doutorando em Matemática UnB, Prof. UFG (Catalão)
• 6a, 29 de Outubro
• 8:30-09:40 Algoritmos Para Pesquisa Aproximada em Palavras,Power Point
Rodrigo de Castro Miranda, Mestrando em Informática UnB
• 09:40-10:10 Coffe-Break
• 10:10-11:20 Prova Automática de Teoremas para Lógicas Modais, PDF
Cláudia Nalon, Prof. Mestrado em Informática UnB, PhD Univ. Liverpool.

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

• 5a, 30 de outubro
• 14:30-16:00 Aspetos Teóricos e Implementacionais do Cálculo Lambda em Ambientes de Substituições Explícitas,
Flávio Leonardo Cavalcanti de Moura
• 16:00-16:20 Coffe-Break
• 16:20-17:50 On-line Approximate String Matching over Space Efficient Suffix Trees,
Leon Solon da Silva
• 6a, 31 de Outubro
• 8:30-10:00 Verificação da Correção de Especificações em Reescrita usando PVS,
Thomas Mailleux Santana
• 10:00-10:20 Coffe-Break
• 10:20-11:50 Deteção e Resolução Formal de Conflitos de Trafego Aéreo,
Valnei Alves Fernandes

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 20th Century.
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

• Ruy de Queiroz (UFPE)
• Mauricio Ayala-Rincón (UnB)
• Salahoddin Shokranian (UnB)
Comunicações por
• Carlos Llanos (UPIS),
• Roberto Callejas-Bedregal (UFPB) e
• Li Weigang (UnB)
Mini-Curso em Biologia Computacional por
• Maria Emilia Walter (UnB),

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


text:
# RD Sharma Solutions for Class 6 Chapter 20: Mensuration Objective Type Questions

This exercise contains objective type questions at the end covering topics from the entire chapter. The solutions contain brief explanations in order to make them easier for the students to understand from the exam point of view. Here, important formulas and topics are highlighted to help students grasp the concepts. The students can gain knowledge on how much they have understood across all concepts. To know more about the important concepts which are covered here, RD Sharma Solutions Class 6 Maths Chapter 20 Mensuration Objective Type Questions are available for free download.

## RD Sharma Solutions for Class 6 Chapter 20: Mensuration Objective Type Questions Download PDF

### Access RD Sharma Solutions for Class 6 Chapter 20: Mensuration Objective Type Questions

Mark the correct alternative in each of the following:

1. The side of a rectangle are in the ratio 5: 4. If its perimeter is 72 cm, then its length is
(a) 40 cm
(b) 20 cm
(c) 30 cm
(d) 60 cm

Solution:

The option (b) is the correct answer.

Consider the sides of the rectangle as 5x and 4x.

We know that, perimeter of rectangle = 2 (Length + Breadth)

By substituting the values

72 = 2 (5x + 4x)

On further calculation

72 = 2 × 9x

So we get

72 = 18x

By division

x = 72/18 = 4

Hence, the length of the rectangle = 5x = 5 × 4 = 20 cm

2. The cost of fencing a rectangular field 34 m long and 18 m wide at Rs 2.25 per metre is
(a) Rs 243
(b) Rs 234
(c) Rs 240
(d) Rs 334

Solution:

The option (b) is the correct answer.

We must find the perimeter of the rectangle for fencing the field.

The dimensions of the rectangle are

Length = 34m

Breadth = 18m

We know that Perimeter = 2 (Length + Breadth)

By substituting the values

Perimeter of the rectangle = 2 (34 + 18) = 2 × 52 = 104 m

So the cost of fencing the field at the rate of Rs. 2.25 per meter = 104 × 2.25 = Rs. 234

3. If the cost of fencing a rectangular field at Rs. 7.50 per metre is Rs. 600, and the length of the field is 24 m, then the breadth of the field is
(a) 8 m
(b) 18 m
(c) 24 m
(d) 16 m

Solution:

The option (d) is the correct answer.

It is given that cost of fencing the rectangular field = Rs. 600

So the rate of fencing the field = Rs. 7.50 per m

We know that perimeter of the field = Cost of fencing/Rate of fencing

By substituting the values

Perimeter of the field = 600/7.50 = 80 m

Length of the field = 24 m

So we get breadth of the field = Perimeter/2- Length = 80/2- 24 = 16 m

4. The cost of putting a fence around a square field at Rs 2.50 per metre is Rs 200. The length of each side of the field is
(a) 80 m
(b) 40 m
(c) 20 m
(d) None of these

Solution:

The option (c) is the correct answer.

It is given that cost of fencing the square field = Rs. 200

So the rate of fencing the field = Rs. 2.50

We know that, perimeter of the square field = Cost of fencing/Rate of fencing

By substituting the values

Perimeter of the square field = 200/2.50 = 80 m

Perimeter of square = 4 × Side of the square

It can be written as

Side of the square = Perimeter/4 = 80/4 = 20 m

5. The length of a rectangle is three times of its width. If the length of the diagonal is 8√10 m, then the perimeter of the rectangle is
(a) 15√10 m
(b) 16√10 m
(c) 24√10 m
(d) 64 m

Solution:

The option (d) is the correct answer.

Consider ABCD as a rectangle.

Assume that the width of the rectangle BC = x m

We know that the length is three times width of the rectangle.

So, length of the rectangle AB = 3x m

AC is the diagonal of rectangle

Consider ABC as a right angled triangle.

AC2 = AB2 + BC2

By substituting the values

640 = 9x2 + x2

We get

640 = 10x2

On further calculation

x2 = 640/10 = 64

x = √64 = 8 m

So the breadth of the rectangle x = 8 m

Length of the rectangle 3x = 3 × 8 = 24 m

Perimeter = 2 (Length + Breadth)

By substituting the values

Perimeter = 2 (24 + 8) = 2 × 32 = 64 m

6. If a diagonal of a rectangle is thrice its smaller side, then its length and breadth are in the ratio
(a) 3: 1
(b) √3: 1
(c) √2 : 1
(d) 2√2: 1

Solution:

The option (d) is the correct answer.

Assume that the length of the smaller side of the rectangle BC = x

Length of the larger side AB = y

We know that the length of the diagonal is three times that of the smaller side.

Diagonal of the rectangle 3x = AC

By using Pythagoras theorem

(AC) 2 = (AB) 2   + (BC) 2

By substituting the values

(3x) 2 = (x) 2 + (y) 2

On further calculation

9x2 = x2 + y2

We get

8x2 = y2

By taking square roots of both sides,

2√2 x = y

Hence, the ratio of the larger side to the smaller side is 2√2: 1.

7. The ratio of the areas of two squares, one having its diagonal double than the other, is
(a) 1: 2
(b) 2: 3
(c) 3: 1
(d) 4: 1

Solution:

The option (d) is the correct answer.

Consider ABCD and PQRS as the two squares. We know that, the diagonal of square PQRS is twice the diagonal of square ABCD.

PR = 2 AC

Area of the square = Diagonal2/2

Area of PQRS = PR2/2

In the same way, area of ABCD = AC2/2

From the question, we know that:

If AC = x units, we get PR = 2x units

Area of PQRS/Area of ABCD = (PR2×2)/ (2×AC2

By substituting the value

Area of PQRS/Area of ABCD = [(2x) 2×2]/ [2×x2] = 4/1

Hence, the ratio of the areas of squares PQRS and ABCD is 4: 1.

8. If the ratio of areas of two squares is 225 : 256, then the ratio of their perimeters is
(a) 225 : 256
(b) 256 : 225
(c) 15 : 16
(d) 16 : 15

Solution:

The option (c) is the correct answer.

Consider ABCD and PQRS as the two squares.

Let the lengths of each side of ABCD and PQRS be x and y.

We know that

Area of sq. ABCD/Area of sq. PQRS = x2/y2

So we get x2/y2= 225/256

By taking square roots on both sides,

x/y = 15/16

By taking the ratio of their perimeters, we get

Perimeter of sq. ABCD/Primeter of sq. PQRS = (4 × side of sq. ABCD)/ (4 × side of sq. PQRS) = 4x/4y

By removing common terms in numerator and denominator

Perimeter of sq. ABCD/Perimeter of sq. PQRS = x/ y

So perimeter of sq. ABCD/Perimeter of sq. PQRS = 15/16

Hence, the ratio of their perimeters = 15: 16

9. If the sides of a square are halved, the its area
(a) remains same
(b) becomes half
(c) becomes one fourth
(d) becomes double

Solution:

The option (c) is the correct answer.

Consider x as the side of the square.

We know that area of a square = Side × Side = x × x = x2

If the sides are halved, we get new side = x/2

So the new area = (x/2)2= x2/4

From this we know that the area has become one fourth of its previous value.

10. A rectangular carpet has area 120 m2 and perimeter 46 metres. The length of its diagonal is
(a) 15 m
(b) 16 m
(c) 17 m
(d) 20 m

Solution:

The option (c) is the correct answer.

It is given that area of the rectangle = 120 m2

Perimeter of the rectangle = 46 m

Consider l and b as the length and breadth.

Area of the rectangle = l × b = 120 m2

Perimeter of the rectangle = 2 (l + b) = 46

So we get

(l + b) = 46/2 = 23 m

Length of the diagonal of the rectangle = √l2 + b2

It can be written as

(l2 + b2) = (l + b) 2 – 2 (l × b)

By substituting the values

(l2 + b2) = (23)2 – 2 (120) = 529 – 240 = 289

Hence, length of the diagonal of the rectangle = √l2 + b2 = √289 = 17 m

11. If the ratio between the length and the perimeter of a rectangular plot is 1: 3, then the ratio between the length and breadth of the plot is
(a) 1: 2
(b) 2: 1
(c) 3: 2
(d) 2: 3

Solution:

The option (b) is the correct answer.

We know that Length of rectangle/Perimeter of rectangle = 1/3

So we get

l/ (2l + 2b) = 1/3

By cross multiplication, we get:

3l = 2l + 2b

On further calculation

l = 2b

We get

l/ b= 2/1

Hence, the ratio of the length and the breadth is 2: 1.

12. If the length of the diagonal of a square is 20 cm, then its perimeter is
(a) 10√2cm
(b) 40 cm
(c) 40√2cm
(d) 200 cm

Solution:

The option (c) is the correct answer.

It is given that length of the diagonal = 20 cm

So the length of the side of a square = Length of Diagonal/√2 = 20/√2 = (2 × 10)/√2

We get

Length of the side of a square = (√2 × √2 × 10)/√2 = 10√2 cm

Hence, perimeter of the square = 4 × Side = 4 ×10√2 = 40√2 cm

format: plain


text:
Torque & Equilibrium Video Lessons

Concept

# Problem: A uniform 300-N trapdoor in a ceiling is hinged at one side.a) Find the net upward force needed to begin to open it, if the upward force is applied at the center of the edge opposite the hinges.b) Find the total force exerted on the door by the hinges, if the upward force is applied at the center of the edge opposite the hinges.

###### FREE Expert Solution

Torque:

$\overline{){\mathbf{\tau }}{\mathbf{=}}{\mathbf{r}}{\mathbf{F}}{\mathbf{s}}{\mathbf{i}}{\mathbf{n}}{\mathbf{\theta }}}$

Newton's second law:

$\overline{){\mathbf{\Sigma F}}{\mathbf{=}}{\mathbf{ma}}}$

Let the length of the door be L.

(a)

The force applied acts at a distance L from the rotational point while the weight acts at L/2 from the hinges.

The forces and radial distance are perpendicular — θ = 90°

ΣT = 0

(L/2)•mgsin 90 - (L)Fapplied sin 90 = 0

###### Problem Details

A uniform 300-N trapdoor in a ceiling is hinged at one side.

a) Find the net upward force needed to begin to open it, if the upward force is applied at the center of the edge opposite the hinges.

b) Find the total force exerted on the door by the hinges, if the upward force is applied at the center of the edge opposite the hinges.

What scientific concept do you need to know in order to solve this problem?

Our tutors have indicated that to solve this problem you will need to apply the Torque & Equilibrium concept. You can view video lessons to learn Torque & Equilibrium. Or if you need more Torque & Equilibrium practice, you can also practice Torque & Equilibrium practice problems.


text:
### The subtle yet real racism of the Supreme Court

Judge Roberts, a member of the highest court in the land, which is currently hearing the sad story of mediocre college aspirant Abigail Fischer, recently asked, "What unique perspective does a minority student bring to a physics class? I’m just wondering what the benefits of diversity are in that situation?"

Did you catch the white supremacy in this question? If not, don't feel bad because it's subtly hidden beneath the cloaking field of colorblind racism. (As for Scalia's ign'nt-ass statements, I'm not even...)

Try rephrasing the question: "What unique perspective does a white student bring to a physics classroom?" The answer is, of course, absolutely nothing! Why? Because race isn't biological, and is therefore not deterministic of cognitive abilities. Did you perhaps forget that you knew that when considering Roberts' question? If so, again, it's understandable. Our society and culture condition all of us to forget basic facts like this.

So isn't this an argument in favor of colorblindness? Since race isn't real, shouldn't we ignore it? It might seem counterintuitive, but the answer is a resounding no. We should not ignore race. We should acknowledge it and it should be made explicit in every aspect of the SCOTUS hearing on affirmative action, as well in our admissions and hiring procedures. Why? Because even though race isn't a biological reality, it is most certainly a societal reality.

Remember, modern-day liberal racism rests on "colorblindness," which in turn rests on the No Racism Axiom, which posits that systemic racism is not a thing. The logical next step from this (false) axiomatic starting point is that everyone has an equal set of opportunities and choices that lead to an equal set of corresponding outcomes. Roberts is implicitly making this specious assumption in framing his question. Since all students have an equal opportunity, then the lack of "minorities" (read: Black, Latin@ and Indigenous students) in a physics classroom is a reflection of either mathematical incompetence, bad choices, or both.

The problem is that extending Roberts' reasoning one step further reveals that this supposed disparity in ability and propensity for bad choices falls along race lines. White (straight, cisgender male) students are, on average, really good at physics and make good choices to get into physics classes at the best universities. Nonwhite students perform poorly at math-oriented tasks and make poor choices along their educational trajectories.

This should lead to the question: but why? Why does race matter? Unfortunately, this is where the logical process falters, and things get "complicated" in the minds of many white people. Instead, we're left with an unanswered question from one of the most powerful figures in our country that reifies race, once again. This is what Karen Fields and Barbara Fields refer to as "Racecraft." Barbara Fields gives an excellent analogy of how questions like Judge Roberts' can make fictional concepts real, even among knowledgeable people (cf also her shorter essay). "How does a witch make someone sick using the evil eye?" The question implicitly acknowledges the reality of witches and witchcraft. Racecraft, y'all!

The intrinsic nature of race and its relationship to physics acumen, and the logical conclusion that the only reason we'd want more "minorities" in a physics classroom is for diversity-based aesthetics is embedded in Roberts' question. It is further reinforced by the defense attorney who weakly responded by citing a study that shows that diversity is good. Apparently the notion that Black students might (gasp!) be really good at physics if given a chance is never given voice the hallowed halls of the Supreme Court. The Justice might as well have asked how unicorns fly and the attorney responded with an explanation of the Bernoulli effect.

However, the extrinsic reasons for the racial disparities in the physics classroom, and elsewhere, are not only knowable, they are well studied and published in hundreds of peer-reviewed papers, books and lectures in the social sciences, psychology and economics. All of these materials are readily available via the a straight-forward Google search, coffee mug and notebook at the ready. The problem for colorblind people is that the answers point back to this thing called "systemic racism," giving lie to the No-Racism Axiom.

For example, the reasons for racial disparities, generally, are nicely summarized in the writing of Gunnar Myrdal, a white Nobel laureate economist, who wrote as far back as 1944 (quoted in Haney Lopez 2013):
Practically all the economic, social, and political power is held by whites...It is thus the white majority group that naturally determines the Negro's 'place.' All our attempts to reach scientific explanations of why the Negroes are what they are and why they live as they do have regularly led to determinations on the white side of the race line.
Even more damning, in the report commissioned by President Johnson in 1967, the Kerner Commission concludes, "Segregation and poverty have created in the [Black community] a destructive environment totally unknown to most white Americans...White institutions created it, white institutions maintain it, and white society condones it."

But isn't this in the past? one might ask. Lemme reach into my pocket and pull out a big Nope from just a couple years ago. A report out of Brandies University (Shapiro, Meschede & Osoro 2013) summarizes the root causes of the present-day 18-to-1 wealth gap between white and Black US-Americans, keeping in mind that wealth is awfully handy in getting a higher education:
Homes are the largest investment that most American families make and by far the biggest item in their wealth portfolio...Yet, for many years, redlining, discriminatory mortgage-lending practices, lack of access to credit, and lower incomes have blocked the homeownership path for African Americans while creating and reinforcing communities segregated by race.
This history of race-based real estate plunder is described in detail here. The state of extreme segregation in public schools is described here. The disparities in educational opportunities in predominantly non-white public schools are described here. The ability of negative racial stereotypes to impact academic performance is laid out in over 300 peer-reviewed journal articles here

Having Black/Brown students in a physics classroom isn't about diversity. It's about basic justice. It's about letting a Black/Brown kid with the audacity and courage to step into any white-dominated academic field to do so, be supported, and ultimately succeed, just like any white student. After all, Ms. Fischer isn't arguing that she'd add diversity to the University of Texas. She feels it was unjust that she wasn't admitted, even if her academic performance proves otherwise despite her white advantage.

The willful ignorance of Judges Roberts and Scalia, and especially for the white defending attorney who had no meaningful answer to Roberts' racist question, is unsurprising, in my view, yet nonetheless disgusting and sad. I just sit here watching how their comments, the extrajudicial killings of Black women and men, the racist comments of carnival barkers masquerading as presidential candidates, the real yet ignored reasons behind the student protests, and white faculty crying about "freedom of speech" are all parts of the same machinery of racial injustice.

I don't know what else to say about US-America's "epistemology of ignorance," as Charles Mills aptly names it. I guess it's a good time to let James Baldwin have the last word:
The record is there for all to read. It resounds all over the world. It might as well be written in the sky. One wishes that Americans—white Americans—would read, for their own sakes, this record and stop defending themselves against it. Only then will they be enabled to change their lives.
No, wait. Check that, and check my male privilege. Let's give Kwanzaa Bennett the last word:
Truly, it’s no surprise that Fisher’s proposed solution is a “colorblind” entry process. Colorblindness has always been a very effective way for white people to pretend to be progressive and “non-racist” while conveniently ignoring the voices and unique challenges of people of color—black people especially...Ms. Fisher, if you ever do feel like having a grown-up conversation about racial discrimination and unfair advantage in America, we’ll be happy to offer you a seat at our table, just as soon as you turn in your five-page essay on the historical disadvantages white people have had in the educational system built on the backs of those who have been forced to attend "separate but equal" schools since their conception. We’ll wait.

### On the Height of J.J. Barea

Dallas Mavericks point guard J.J. Barea standing between two very tall people (from: Picassa user photoasisphoto).

Congrats to the Dallas Mavericks, who beat the Miami Heat tonight in game six to win the NBA championship.

Okay, with that out of the way, just how tall is the busy-footed Maverick point guard J.J. Barea? He's listed as 6-foot on NBA.com, but no one, not even the sports casters, believes that he can possibly be that tall. He looks like a super-fast Hobbit out there. But could that just be relative scaling, with him standing next to a bunch of extremely tall people? People on Yahoo! Answers think so---I know because I've been Google searching "J.J. Barea Height" for the past 15 minutes.

So I decided to find a photo and settle the issue once and for all.

I started by downloading a stock photo of J.J. from NBA.com, which I then loaded into OpenOffice Draw:

I then used the basketball as my metric. Wikipedia states that an NBA basketball is 29.5 inches in circumfe…

### Finding Blissful Clarity by Tuning Out

It's been a minute since I've posted here. My last post was back in April, so it has actually been something like 193,000 minutes, but I like how the kids say "it's been a minute," so I'll stick with that.
As I've said before, I use this space to work out the truths in my life. Writing is a valuable way of taking the non-linear jumble of thoughts in my head and linearizing them by putting them down on the page. In short, writing helps me figure things out. However, logical thinking is not the only way of knowing the world. Another way is to recognize, listen to, and trust one's emotions. Yes, emotions are important for figuring things out.
Back in April, when I last posted here, my emotions were largely characterized by fear, sadness, anger, frustration, confusion and despair. I say largely, because this is what I was feeling on large scales; the world outside of my immediate influence. On smaller scales, where my wife, children and friends reside, I…

### The Force is strong with this one...

Last night we were reviewing multiplication tables with Owen. The family fired off doublets of numbers and Owen confidently multiplied away. In the middle of the review Owen stopped and said, "I noticed something. 2 times 2 is 4. If you subtract 1 it's 3. That's equal to taking 2 and adding 1, and then taking 2 and subtracting 1, and multiplying. So 1 times 3 is 2 times 2 minus 1."

I have to admit, that I didn't quite get it at first. I asked him to repeat with another number and he did with six: "6 times 6 is 36. 36 minus 1 is 35. That's the same as 6-1 times 6+1, which is 35."

Ummmmm....wait. Huh? Lemme see...oh. OH! WOW! Owen figured out

x^2 - 1 = (x - 1) (x +1)

So $6 \times 8 = 7 \times 7 - 1 = (7-1) (7+1) = 48$. That's actually pretty handy!

You can see it in the image above. Look at the elements perpendicular to the diagonal. There's 48 bracketing 49, 35 bracketing 36, etc... After a bit more thought we…


text:
# How do you find the derivative of f(x)=x^3+x^2 using the limit process?

Nov 10, 2016

$f ' \left(x\right) = 3 {x}^{2} + 2 x$

#### Explanation:

By definition of the derivative $f ' \left(x\right) = {\lim}_{h \rightarrow 0} \frac{f \left(x + h\right) - f \left(x\right)}{h}$
So with $f \left(x\right) = {x}^{3} + {x}^{2}$ we have;

$f ' \left(x\right) = {\lim}_{h \rightarrow 0} \frac{\left\{{\left(x + h\right)}^{3} + {\left(x + h\right)}^{2}\right\} - \left\{{x}^{3} + {x}^{2}\right\}}{h}$
$\therefore f ' \left(x\right) = {\lim}_{h \rightarrow 0} \frac{{x}^{3} + 3 {x}^{2} h + 3 x {h}^{2} + {h}^{3} + {x}^{2} + 2 h x + {h}^{2} - {x}^{3} - {x}^{2}}{h}$
$\therefore f ' \left(x\right) = {\lim}_{h \rightarrow 0} \frac{3 {x}^{2} h + 3 x {h}^{2} + {h}^{3} + 2 h x + {h}^{2}}{h}$
$\therefore f ' \left(x\right) = {\lim}_{h \rightarrow 0} \left(3 {x}^{2} + 3 x h + {h}^{2} + 2 x + h\right)$
$\therefore f ' \left(x\right) = 3 {x}^{2} + 2 x$


text:
Question

# For a real gas the P-V curve was experimentally plotted and it had the following appearance. With respect to liquefaction. Choose the correct statement

A
At T=500 K, P=40 atm, the state will be liquid
B
At T=300 K, P=50 atm, the state will be gas
C
At T<300 K, P=20 atm, the state will be gas
D
At 300 K<T<500 K,P>50 atm, the state will be liquid

Solution

## The correct option is D At 300 K<T<500 K,P>50 atm, the state will be liquidObservations from graph are: (a) At T=500 K,P=40 atm corresponds to 'a' substance - gas (b) At T=300 K,P=50 atm corresponds to 'b' substance -  liquid (c) At T=300 K,P>20 atm corresponds to 'c' substance -  liquid (d) At 300 K<T<500 K,P>50 atm, corresponds to 'd' substance -  liquid So, correct option is (d).Chemistry

Suggest Corrections

0

Similar questions
View More

People also searched for
View More


text:
## CryptoDB

### Paper: CAPA: The Spirit of Beaver Against Physical Attacks

Authors: Oscar Reparaz Lauren De Meyer Begül Bilgin Victor Arribas Svetla Nikova Ventzislav Nikov Nigel P. Smart DOI: 10.1007/978-3-319-96884-1_5 Search ePrint Search Google Slides CRYPTO 2018 In this paper we introduce two things: On one hand we introduce the Tile-Probe-and-Fault model, a model generalising the wire-probe model of Ishai et al. extending it to cover both more realistic side-channel leakage scenarios on a chip and also to cover fault and combined attacks. Secondly we introduce CAPA: a combined Countermeasure Against Physical Attacks. Our countermeasure is motivated by our model, and aims to provide security against higher-order SCA, multiple-shot FA and combined attacks. The tile-probe-and-fault model leads one to naturally look (by analogy) at actively secure multi-party computation protocols. Indeed, CAPA draws much inspiration from the MPC protocol SPDZ. So as to demonstrate that the model, and the CAPA countermeasure, are not just theoretical constructions, but could also serve to build practical countermeasures, we present initial experiments of proof-of-concept designs using the CAPA methodology. Namely, a hardware implementation of the KATAN and AES block ciphers, as well as a software bitsliced AES S-box implementation. We demonstrate experimentally that the design can resist second-order DPA attacks, even when the attacker is presented with many hundreds of thousands of traces. In addition our proof-of-concept can also detect faults within our model with high probability in accordance to the methodology.
##### BibTeX
@inproceedings{crypto-2018-28862,
title={CAPA: The Spirit of Beaver Against Physical Attacks},
booktitle={Advances in Cryptology – CRYPTO 2018},
series={Lecture Notes in Computer Science},
publisher={Springer},
volume={10991},
pages={121-151},
doi={10.1007/978-3-319-96884-1_5},
author={Oscar Reparaz and Lauren De Meyer and Begül Bilgin and Victor Arribas and Svetla Nikova and Ventzislav Nikov and Nigel P. Smart},
year=2018
}


text:
# from the previous task (Hopfield model with wii = 0 and with stochastic updating) check the phase diagram drawn on p. 63 of the lecture notes. (a). Choose the

2017-02-20

den of GPS phase ambiguity resolution in a CORS RTK Network. Journal of 5' 00" 30. Tropospheric model: Hopfield. Hopfield. Ionospheric model:. av H Malmgren · Citerat av 7 — In the learning phase the activity in the resonant layer mirrors input.

The diution is random but symmetric. Phase diagrams are presented for c = 1,o.1,o.ool and c-0, where c is the fractional connectivity. The line Tc memory states become global minima (having lower Iree energy than the spin glass states) is also found for different values of c. It is found that the effect of dilution is to destabilize the The ground-state phase diagram of the Hopﬁeld model in a transverse ﬁeld. “R-I” stands for the retrieval phase in which t he retrieval states are the global minima, and “R-II” denotes 2017-02-20 · Title: Phase Diagram of Restricted Boltzmann Machines and Generalised Hopfield Networks with Arbitrary Priors Authors: Adriano Barra , Giuseppe Genovese , Peter Sollich , Daniele Tantari (Submitted on 20 Feb 2017 ( v1 ), last revised 29 Jul 2017 (this version, v2)) 2001-06-01 · In Fig. 1 we present the phase diagram of the Hopfield model obtained analytically and assuming a replica symmetric Ansatz . Above the T g line the system has a paramagnetic solution with an associated simple homogeneous dynamics. 338 13 The Hopﬁeld Model be described with simple linear algebraic methods.

## Figure 4.1: Phase diagram for the Hopfield model. The system exhibit three different phases. Under the curve TC the phase is ferromagnetic: the states with m = 0

Naef, Jean-Pierre. Published in Journal de Physique I. 1992, vol. 2, no.

### Phase diagrams and the instability of the spin glass states for the diluted Hopfield neural network model: Authors : Canning, Andréw Magnus. Naef, Jean-Pierre. Published in Journal de Physique I. 1992, vol. 2, no. 9, p. 1791-1801 Abstract

Owl may thus represent a model to study density fluctuations, especially in phase was between 7 May (a late spring) and early June. The mean burrow length  som leder till det övre högra hörnet av Hertzsprung-Russell-diagrammet). En alternativ modell som gör att den vita dvärgen stadigt kan ackumulera refraktion är Hopfields och Saasatamoinens atmosfärsmodeller. Kepler's Optical Phase Curve of the Exoplanet HAT-P-7b (http:/ / adsabs. harvard. edu/ abs/ 2009Sci. Hopfield eller aastamonien, men ingen av dem betraktas som standard för GP. Effekten 18 Kapitel 11: Grundläggande teori om GN 11.7 Matematisk modell för  A model of intracellular signalling can implement radial basis function learning in Hopfield has suggested a form of temporal encoding in the brain where using the timing of action potentials relative to the phase of collective subthresho.

Application to the models This section shows the phase diagrams of the Hamiltonian (3).
Installera mobilt bank id

First, we review the “relativistic” Hopfield model and we briefly describe the experimental evidence underlying correlation among patterns. The goal of the present work is to investigate the role of trivial disorder and nontrivial disorder in the three-state Hopfield model under a Gaussian random field.

It does not (indeed cannot) distinguish between these two situations when the weights are being set. Summary of Hopfield Network Equations Weight setting (training) for n memories in an N node Hopfield Network - Ground-state phase diagram as a function of U ∞, μ, and t (in units of U 0) obtained by numerically determining the phases using the mean-field model of Eq. . The MI phase is gray, the CDW is yellow, the SS is red, and the rest of the phase diagram is SF. Note that the tunneling rate is rescaled by the coordination number z (here z = 4). The calculation is tested by computer simulation.

terminator dark fate
camping stockholms län
relationellt perspektiv i förskolan
gym nyc
roland kirk volunteered slavery
vinbaren varberg öppettider

### av V Svensson · 2018 · Citerat av 1 — station set up with network RTK, and in this study, four different methods Figur 3: Diagram som visar hur jonosfärstörningarna var den 5 april,. 2018, d.v.s. den of GPS phase ambiguity resolution in a CORS RTK Network. Journal of 5' 00" 30. Tropospheric model: Hopfield. Hopfield. Ionospheric model:.

Journal of 5' 00" 30. Tropospheric model: Hopfield. Hopfield. Ionospheric model:. av H Malmgren · Citerat av 7 — In the learning phase the activity in the resonant layer mirrors input.

## The phase diagram coincides very accurately with that of the conventional classical Hopfield model if we replace the temperature T in the latter model by $\Delta$.

In this work, we introduce and investigate the properties of the “relativistic” Hopfield model endowed with temporally correlated patterns. First, we review the “relativistic” Hopfield model and we briefly describe the experimental evidence underlying correlation among patterns. Phase diagrams and the instability of the spin glass states for the diluted Hopfield neural network model. In: Journal de Physique I, 1992, vol. 2, As 0, m approaches the value (3.5) at low T .

In this video I present the graphs used in visualizing the Ramsey Cass Koopmans model. The Hopfield model , consists of a network of N N neurons, labeled by a lower index i i, with 1 ≤ i ≤ N 1\leq i\leq N. Similar to some earlier models (335; 304; 549), neurons in the Hopfield model … 1992-11-01 The phase diagrams of the model with finite patterns show that there exist annealing paths that avoid first-order transitions at least for . The same is true for the extensive case with k = 4 and 5. In contrast, it is impossible to avoid first-order transitions for the case of finite patterns with k = 3 and the case of extensive number of patterns with k = 2 and 3. CSE 5526: Hopfield Nets 5 Hopfield (1982) describes the problem • “Any physical system whose dynamics in phase space is dominated by a substantial number of locally stable states to which it is attracted can therefore be regarded as a general content-addressable memory. The physical system will be a potentially useful memory if, in addition 2017-10-27 Phase diagram of restricted Boltzmann machines and generalized Hopfield networks with arbitrary priors Our analysis shows that the presence of a retrieval phase is robust and not peculiar to the standard Hopfield model with Boolean patterns. The retrieval region becomes larger when the pattern entries and retrieval units get 2018-06-26 Basins of attraction - catchment areas around each minimum Energy landscape x1 x2 Hopfield model: attractors are minima of the energy function Additional spurious minima: mixture states (such as ) Load parameter a= p/N For small enough p, the stored patterns xm are attractors of the dynamics – i.e.


text:
# Financial Instruments and Markets - Help needed

Question 5:

ABC Ltd (in thousands of dollars)

 Assets Liabilities Two-year treasury bond $175 One-year CD$135 15-year corporate bond $165 Five-year deposit$160

Notes: All securities are selling at par (equal to book value). The two-year Treasury bonds yield 5 per cent; the 15-year corporate bonds yield 9 per cent; the one-year CD issue pays 4.5 per cent; and the five-year deposit pays 8 per cent. Assume that all instruments have annual coupon payments.

(a) What is the value of ABC Ltds equity?

(b) What is the weighted average maturity of the FIs assets?

(c) What is the weighted average maturity of the FIs liabilities?

(d) What is the FIs maturity gap?

(e) What does your answer in part (d) imply about the interest rate risk exposure on ABC Ltd?

(f) Calculate the values of all four securities on ABC Ltds balance sheet if all interest rates increase by 2 per cent.

(g) What is the impact on the equity of ABC Ltd? Calculate the percentage change in the value of equity.

(h) What would be the impact on ABC Ltds interest rate risk exposure if its liabilities paid interest semi-annually as opposed to annually?