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)
- 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.