Titlebook: Rewriting and Typed Lambda Calculi; Joint International Gilles Dowek Conference proceedings 2014 Springer International Publishing Switzer

Mri485

摘要记录

Jogging

Tree Automata with Height Constraints between Brothers, restrict the applicability of the rules are allowed in ... These constraints allow to express natural tree languages like complete or balanced (like AVL) trees. We prove decidability of emptiness and finiteness for .., and also for a more general class that additionally allows to combine equality a

Confidential

An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting,tic Turing machine. The main novelty of the characterization is that it allows very liberal properties of term rewriting, in particular non-deterministic evaluation: no reduction strategy is enforced, and systems are allowed to be non-confluent.

生命

CURT

共和国

Self Types for Dependently Typed Lambda Encodings,art with a type-assignment form of the Calculus of Constructions, restricted recursive definitions and Miquel’s implicit product. We add a type construct ..., called a ., which allows . to refer to the subject of typing. We show how the resulting System . with this novel form of dependency supports

Medley

First-Order Formative Rules,, formative rules allow dropping some of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, the first-order setting allows for significant improvements of the technique.

Antagonist

Automated Complexity Analysis Based on Context-Sensitive Rewriting,on reduction orders. We show how the monotonicity condition for orders can be weakened by using the notion of context-sensitive rewriting. The presented technique is very easy to implement, even in a modular setting, and has been integrated in the Tyrolean Complexity Tool. We provide ample experimen

headway