Gilles Dowek
Proceedings of the Joint International Conference of the 25th International Conference on Rewriting Techniques and Applications and the 12th International Conference on Typed Lambda Calculi and Applications
RTA-TLCA, 2014.

@proceedings{RTA-TLCA-2014,
	address       = "Vienna, Austria",
	editor        = "Gilles Dowek",
	isbn          = "978-3-319-08917-1",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Joint International Conference of the 25th International Conference on Rewriting Techniques and Applications and the 12th International Conference on Typed Lambda Calculi and Applications}",
	volume        = 8560,
	year          = 2014,
}

Contents (31 items)

5 ×#proving
4 ×#confluence
4 ×#type system
4 ×#λ-calculus
3 ×#analysis
2 ×#automation
2 ×#complexity
2 ×#diagrams
2 ×#logic
2 ×#termination

RTA-TLCA-2014-HondaYB #interactive #process #π-calculus

Process Types as a Descriptive Tool for Interaction — Control and the π-Calculus (KH, NY, MB), pp. 1–20.

RTA-TLCA-2014-Schmidt-Schauss #analysis #concurrent #programming language #semantics

Concurrent Programming Languages and Methods for Semantic Analyses (MSS), pp. 21–30.

RTA-TLCA-2014-Setzer0PT #pattern matching

Unnesting of Copatterns (AS, AA, BP, DT), pp. 31–45.

RTA-TLCA-2014-AotoTU #confluence #diagrams #proving #term rewriting

Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (TA, YT, KU), pp. 46–60.

RTA-TLCA-2014-BaeM #abstraction

Predicate Abstraction of Rewrite Theories (KB, JM), pp. 61–76.

RTA-TLCA-2014-AubertB #unification

Unification and Logarithmic Space (CA, MB), pp. 77–92.

RTA-TLCA-2014-BerardiS #theorem

Ramsey Theorem as an Intuitionistic Property of Well Founded Relations (SB, SS), pp. 93–107.

RTA-TLCA-2014-BizjakBM #nondeterminism #type system

A Model of Countable Nondeterminism in Guarded Type Theory (AB, LB, MM), pp. 108–123.

RTA-TLCA-2014-Burel

Cut Admissibility by Saturation (GB), pp. 124–138.

RTA-TLCA-2014-CreusG #automation #context-free grammar #evaluation

Automatic Evaluation of Context-Free Grammars (CC, GG), pp. 139–148.

RTA-TLCA-2014-CreusG14a #automaton #constraints

Tree Automata with Height Constraints between Brothers (CC, GG), pp. 149–163.

RTA-TLCA-2014-Czajka #confluence #induction #proving #λ-calculus

A Coinductive Confluence Proof for Infinitary λ-Calculus (LC), pp. 164–178.

RTA-TLCA-2014-CarvalhoS #decidability #polynomial #set

An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting (DdC, JGS), pp. 179–193.

RTA-TLCA-2014-Dezani-CiancagliniG #precise #type system

Preciseness of Subtyping on Intersection and Union Types (MDC, SG), pp. 194–207.

RTA-TLCA-2014-EscardoS #data type #type system

Abstract Datatypes for Real Numbers in Type Theory (MHE, AS), pp. 208–223.

RTA-TLCA-2014-FuS #encoding

Self Types for Dependently Typed λ Encodings (PF, AS), pp. 224–239.

RTA-TLCA-2014-FuhsK #first-order

First-Order Formative Rules (CF, CK), pp. 240–256.

RTA-TLCA-2014-HirokawaM #analysis #automation #complexity

Automated Complexity Analysis Based on Context-Sensitive Rewriting (NH, GM), pp. 257–271.

RTA-TLCA-2014-LiuDJ #analysis #confluence

Confluence by Critical Pair Analysis (JL, ND, JPJ), pp. 287–302.

RTA-TLCA-2014-LombardiRV #proving

Proof Terms for Infinitary Rewriting (CL, AR, RdV), pp. 303–318.

RTA-TLCA-2014-Maieli #proving

Construction of Retractile Proof Structures (RM), pp. 319–333.

RTA-TLCA-2014-Mellies #diagrams #string

Local States in String Diagrams (PAM), pp. 334–348.

RTA-TLCA-2014-NakazawaN #reduction #λ-calculus #μ-calculus

Reduction System for Extensional Λμ Calculus (KN, TN), pp. 349–363.

RTA-TLCA-2014-RouxD #type system

The Structural Theory of Pure Type Systems (CR, FvD), pp. 364–378.

RTA-TLCA-2014-Schmidt-SchaussS #call-by #λ-calculus

Applicative May- and Should-Simulation in the Call-by-Value λ Calculus with AMB (MSS, DS), pp. 379–394.

RTA-TLCA-2014-Schmitz #logic

Implicational Relevance Logic is 2-ExpTime-Complete (SS), pp. 395–409.

RTA-TLCA-2014-Statman #λ-calculus

Near Semi-rings and λ Calculus (RS), pp. 410–424.

RTA-TLCA-2014-StefanescuCMMSR #logic #reachability

All-Path Reachability Logic (AS, SC, RM, BMM, TFS, GR), pp. 425–440.

RTA-TLCA-2014-SternagelT #algebra #certification #complexity #formal method #proving #termination

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs (CS, RT), pp. 441–455.

RTA-TLCA-2014-SternagelM #confluence

Conditional Confluence (TS, AM), pp. 456–465.

RTA-TLCA-2014-ZantemaKB #termination

Termination of Cycle Rewriting (HZ, BK, HJSB), pp. 476–490.