VSL 2014: VIENNA SUMMER OF LOGIC 2014

This page contains an index consisting of author-provided keywords.

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

Disclaimer | Powered by EasyChair Smart Program