Masahito Hasegawa
Proceedings of the 11th International Conference on Typed Lambda Calculi and Applications
TLCA, 2013.

@proceedings{TLCA-2013,
	address       = "Eindhoven, The Netherlands",
	doi           = "10.1007/978-3-642-38946-7",
	editor        = "Masahito Hasegawa",
	isbn          = "['978-3-642-38945-0', '978-3-642-38946-7']",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 11th International Conference on Typed Lambda Calculi and Applications}",
	volume        = 7941,
	year          = 2013,
}

Contents (18 items)

2 ×#game studies
2 ×#logic
2 ×#modelling
2 ×#normalisation
2 ×#recursion
2 ×#type system

TLCA-2013-Peyton-Jones #compilation #haskell

Type-Directed Compilation in the Wild: Haskell and Core (SLPJ), p. 1.

TLCA-2013-Herbelin #proving

Proving with Side Effects (HH), p. 2.

TLCA-2013-Mazza #metric

Non-linearity as the Metric Completion of Linearity (DM), pp. 3–14.

TLCA-2013-AhnSFP #system f

System F i (KYA, TS, MPF, AMP), pp. 15–30.

TLCA-2013-AschieriZ #nondeterminism #normalisation

Non-determinism, Non-termination and the Strong Normalization of System T (FA, MZ), pp. 31–47.

TLCA-2013-BentonHN #generative #logic

Proof-Relevant Logical Relations for Name Generation (NB, MH, VN), pp. 48–60.

TLCA-2013-BerardiT #backtracking #game studies #logic #semantics #subclass

Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics (SB, MT), pp. 61–76.

TLCA-2013-Blot #game studies

Realizability for Peano Arithmetic with Winning Conditions in HON Games (VB), pp. 77–92.

TLCA-2013-Breuvart #relational #λ-calculus

The Resource λ Calculus Is Short-Sighted in Its Relational Model (FB), pp. 93–108.

TLCA-2013-Clairambault #bound #linear #reduction

Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head Reduction (PC), pp. 109–124.

TLCA-2013-DudderMR #type system

Intersection Type Matching with Subtyping (BD, MM, JR), pp. 125–139.

TLCA-2013-FridlenderP #algorithm #evaluation #normalisation #type system

A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation (DF, MP), pp. 140–155.

TLCA-2013-HancockMGMA #induction #recursion

Small Induction Recursion (PH, CM, NG, LM, TA), pp. 156–172.

TLCA-2013-KrausECA #theorem

Generalizations of Hedberg’s Theorem (NK, MHE, TC, TA), pp. 173–188.

TLCA-2013-SalvatiW #modelling #recursion #using

Using Models to Model-Check Recursive Schemes (SS, IW), pp. 189–204.

TLCA-2013-Schopp #continuation #interactive #on the

On Interaction, Continuations and Defunctionalization (US), pp. 205–220.

TLCA-2013-SeveriV #modelling #source code

Completeness of Conversion between Reactive Programs for Ultrametric Models (PS, FJdV), pp. 221–235.

TLCA-2013-XuE

A Constructive Model of Uniform Continuity (CX, MHE), pp. 236–249.