-homotopy and refinement of observation. II: Adding new -homotopy equivalences.
Taclets: a new paradigm for constructing interactive theorem provers.
Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules...
Tamaño medio de árboles simplificados.
Estudiamos la media y la varianza del tamaño de los árboles simplificados obtenidos a partir de árboles p-arios y generales. Se demuestra que ambos parámetros son lineales en el tamaño del input. Pero lo que creemos más interesante del artículo es la metodología seguida, que pensamos podría aplicarse al análisis de gran parte de algoritmos de simplificación sobre árboles. Tal técnica involucra un estudio de ciertas series de potencias formales, y la aplicación del teorema de Darboux-Polya para aproximaciones...
Tenseurs et machines
Tensor product of partially-additive monoids.
Teoria dei domini nell’interpretazione astratta: equazioni, completezza e logica
Termination checking with types
The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is...
Termination checking with types
The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose ...
Tests de primalité d'après Adleman, Rumely, Pomerance et Lenstra
Thaw: a tool for approximating cut loci on a triangulation of a surface.
The problem as a string rewriting system.
The problem, generalized Pascal triangles and cellular automata
The Algebraic Degree of Geometric Optimization Problems.
The alternation hierarchy for the theory of -lattices.
The asymptotic spectrum of tensors.
The behaviour of parsing time under grammar morphisms
The branching nerve of HDA and the Kan condition.
The brownian motion : a neglected tool for the complexity analysis of sorted tables manipulation
The calculus of an unnormalized relational model of data
The category of Pawlak machines