RTA-TLCA 2014 LNCS PROCEEDINGS: KEYWORD INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E F G H I L M N O P R S T U W

A
abstract datatypes	Abstract datatypes for real numbers in type theory (PDF, talk)
algebraic data types	Unnesting of Copatterns (PDF, talk)
amortised resource analysis	Amortised Resource Analysis and Typed Polynomial Interpretations (PDF, talk)
Automata	Automatic Evaluation of Context-Free Grammars (System Description) (PDF, talk)
automation	Automated Complexity Analysis Based on Context-Sensitive Rewriting (PDF, talk) Conditional Confluence (System Description) (PDF, talk)
axiomatic semantics	All-Path Reachability Logic (PDF, talk)
B
bisimulation	Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB (PDF, talk)
branching VASS	Implicational Relevance Logic is 2-ExpTime-Complete (PDF, talk)
C
certification	Formalizing monotone algebras for certification of termination- and complexity proofs (PDF, talk)
Church-Rosser	Confluence by Critical Pair Analysis (PDF, talk)
coalgebras	Unnesting of Copatterns (PDF, talk)
codata	Unnesting of Copatterns (PDF, talk)
coinduction	A Coinductive Confluence Proof for Infinitary Lambda-Calculus. (PDF, talk)
combinatorics	Ramsey Theorem as an intuitionistic property of well founded relations (PDF, talk)
completion	Cut Admissibility by Saturation (PDF, talk)
complexity	Implicational Relevance Logic is 2-ExpTime-Complete (PDF, talk) Formalizing monotone algebras for certification of termination- and complexity proofs (PDF, talk)
complexity analysis	Automated Complexity Analysis Based on Context-Sensitive Rewriting (PDF, talk)
complexity of rewriting	Amortised Resource Analysis and Typed Polynomial Interpretations (PDF, talk)
compression	Proof terms for infinitary rewriting (PDF, talk)
concurrency	All-Path Reachability Logic (PDF, talk)
conditional rewriting	Cut Admissibility by Saturation (PDF, talk)
conditional term rewriting	Conditional Confluence (System Description) (PDF, talk)
confluence	Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (PDF, talk) A Coinductive Confluence Proof for Infinitary Lambda-Calculus. (PDF, talk) Reduction System for Extensional Lambda-mu Calculus (PDF, talk) Conditional Confluence (System Description) (PDF, talk)
conservative extension	Unnesting of Copatterns (PDF, talk) The Structural Theory of Pure Type Systems (PDF, talk)
Constraints	Tree Automata with Height Constraints between Brothers (PDF, talk)
constructive mathematics	Ramsey Theorem as an intuitionistic property of well founded relations (PDF, talk)
context-sensitive rewriting	Automated Complexity Analysis Based on Context-Sensitive Rewriting (PDF, talk)
contextual equivalence	Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB (PDF, talk)
copattern matching	Unnesting of Copatterns (PDF, talk)
countable choice	A Model of Countable Nondeterminism in Guarded Type Theory (PDF, talk)
critical pairs	Confluence by Critical Pair Analysis (PDF, talk)
Cycle rewriting	Termination of Cycle Rewriting (PDF, talk)
D
Decreasing Diagrams	Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (PDF, talk) Confluence by Critical Pair Analysis (PDF, talk)
deduction modulo	Cut Admissibility by Saturation (PDF, talk)
dependent elimination	Self Types for Dependently Typed Lambda Encodings (PDF, talk)
Dependent types	Self Types for Dependently Typed Lambda Encodings (PDF, talk)
Derivational complexity	Termination of Cycle Rewriting (PDF, talk)
E
Emptiness	Tree Automata with Height Constraints between Brothers (PDF, talk)
equivalence	Automatic Evaluation of Context-Free Grammars (System Description) (PDF, talk)
exact real-number computation	Abstract datatypes for real numbers in type theory (PDF, talk)
extensional model	Reduction System for Extensional Lambda-mu Calculus (PDF, talk)
F
Finiteness	Tree Automata with Height Constraints between Brothers (PDF, talk)
first-order term rewriting	First-Order Formative Rules (PDF, talk)
focusing proofs	Construction of retractile proof structures (PDF, talk) Implicational Relevance Logic is 2-ExpTime-Complete (PDF, talk)
G
Geometry of Interaction	Unification and Logarithmic Space (PDF, talk)
Graded theories	Local states in string diagrams (PDF, talk)
grammars	Automatic Evaluation of Context-Free Grammars (System Description) (PDF, talk)
graph rewriting	Construction of retractile proof structures (PDF, talk)
guarded recursion	A Model of Countable Nondeterminism in Guarded Type Theory (PDF, talk)
H
hashing	Automatic Evaluation of Context-Free Grammars (System Description) (PDF, talk)
higher-order term rewriting	First-Order Formative Rules (PDF, talk)
I
Implicit Complexity	Unification and Logarithmic Space (PDF, talk)
implicit computational complexity	An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting (PDF, talk)
inductive definitions	Ramsey Theorem as an intuitionistic property of well founded relations (PDF, talk)
infinitary lambda-calculus	A Coinductive Confluence Proof for Infinitary Lambda-Calculus. (PDF, talk)
infinitary rewriting	A Coinductive Confluence Proof for Infinitary Lambda-Calculus. (PDF, talk) Proof terms for infinitary rewriting (PDF, talk)
Intersection and Union Types	Preciseness of subtyping on intersection and union types (PDF, talk)
L
lambda calculus	Preciseness of subtyping on intersection and union types (PDF, talk) Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB (PDF, talk) Near semi-rings and lambda calculus (PDF, talk)
Lambda encodings	Self Types for Dependently Typed Lambda Encodings (PDF, talk)
lambda-mu calculus	Reduction System for Extensional Lambda-mu Calculus (PDF, talk)
Lawvere theories	Local states in string diagrams (PDF, talk)
linear logic	Construction of retractile proof structures (PDF, talk)
Logarithmic Space	Unification and Logarithmic Space (PDF, talk)
M
model checking	Predicate Abstraction of Rewrite Theories (PDF, talk)
Modularity	Confluence by Critical Pair Analysis (PDF, talk)
Monads with arities	Local states in string diagrams (PDF, talk)
N
near semi-rings	Near semi-rings and lambda calculus (PDF, talk)
Non-Linear	Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (PDF, talk)
Non-orthogonality	An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting (PDF, talk)
nondeterminism	Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB (PDF, talk)
O
operational semantics	All-Path Reachability Logic (PDF, talk)
P
Pattern matching	Unnesting of Copatterns (PDF, talk)
permutation equivalence	Proof terms for infinitary rewriting (PDF, talk)
Persistency	Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (PDF, talk)
Pointer Machines	Unification and Logarithmic Space (PDF, talk)
polynomial interpretations	Amortised Resource Analysis and Typed Polynomial Interpretations (PDF, talk)
predicate abstraction	Predicate Abstraction of Rewrite Theories (PDF, talk)
predicativity	The Structural Theory of Pure Type Systems (PDF, talk)
Presheaf semantics	Local states in string diagrams (PDF, talk)
program equivalence	A Model of Countable Nondeterminism in Guarded Type Theory (PDF, talk)
program verification	All-Path Reachability Logic (PDF, talk)
proof construction	Construction of retractile proof structures (PDF, talk)
proof nets	Construction of retractile proof structures (PDF, talk)
proof nets retraction	Construction of retractile proof structures (PDF, talk)
proof search	Construction of retractile proof structures (PDF, talk)
proof terms	Proof terms for infinitary rewriting (PDF, talk)
proof theory	Unification and Logarithmic Space (PDF, talk)
Pure Type Systems	The Structural Theory of Pure Type Systems (PDF, talk)
R
Reachability problem	An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting (PDF, talk)
relevance logic	Implicational Relevance Logic is 2-ExpTime-Complete (PDF, talk)
resolution and superposition	Cut Admissibility by Saturation (PDF, talk)
Rewriting	Confluence by Critical Pair Analysis (PDF, talk)
rewriting logic	Predicate Abstraction of Rewrite Theories (PDF, talk)
Rule-Labelling	Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (PDF, talk)
S
SAT	Automatic Evaluation of Context-Free Grammars (System Description) (PDF, talk)
semantics	Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB (PDF, talk)
sequent calculus	Cut Admissibility by Saturation (PDF, talk) Construction of retractile proof structures (PDF, talk)
step-indexing	A Model of Countable Nondeterminism in Guarded Type Theory (PDF, talk)
string rewriting	Termination of Cycle Rewriting (PDF, talk)
Strong normalisation	Unnesting of Copatterns (PDF, talk)
strong normalization	Reduction System for Extensional Lambda-mu Calculus (PDF, talk)
subtyping	Preciseness of subtyping on intersection and union types (PDF, talk)
System description	Nagoya Termination Tool (PDF, talk)
System T	Abstract datatypes for real numbers in type theory (PDF, talk)
T
term rewriting	Automated Complexity Analysis Based on Context-Sensitive Rewriting (PDF, talk) Amortised Resource Analysis and Typed Polynomial Interpretations (PDF, talk) Nagoya Termination Tool (PDF, talk)
Term rewriting system	An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting (PDF, talk)
Term rewriting systems	Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (PDF, talk)
termination	Formalizing monotone algebras for certification of termination- and complexity proofs (PDF, talk) Nagoya Termination Tool (PDF, talk) Termination of Cycle Rewriting (PDF, talk)
termination analysis	First-Order Formative Rules (PDF, talk)
the B I monoid	Near semi-rings and lambda calculus (PDF, talk)
The dependency pair framework	Nagoya Termination Tool (PDF, talk)
the game of Alonzo	Near semi-rings and lambda calculus (PDF, talk)
theorem proving	Formalizing monotone algebras for certification of termination- and complexity proofs (PDF, talk)
transfinite reduction	Proof terms for infinitary rewriting (PDF, talk)
Tree-Automata	Tree Automata with Height Constraints between Brothers (PDF, talk)
type theory	The Structural Theory of Pure Type Systems (PDF, talk)
typed lambda-calculus	Abstract datatypes for real numbers in type theory (PDF, talk)
Types	Amortised Resource Analysis and Typed Polynomial Interpretations (PDF, talk)
U
Unification	Unification and Logarithmic Space (PDF, talk)
usable rules	First-Order Formative Rules (PDF, talk)
W
weak normalization	The Structural Theory of Pure Type Systems (PDF, talk)
while-programs	Ramsey Theorem as an intuitionistic property of well founded relations (PDF, talk)