Jean-Yves Girard
Proceedings of the Fourth International Conference on Typed Lambda Calculi and Applications
TLCA, 1999.

@proceedings{TLCA-1999,
	address       = "L'Aquila, Italy",
	editor        = "Jean-Yves Girard",
	isbn          = "3-540-65763-0",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fourth International Conference on Typed Lambda Calculi and Applications}",
	volume        = 1581,
	year          = 1999,
}

Contents (27 items)

7 ×#logic
3 ×#linear
3 ×#semantics
3 ×#λ-calculus
2 ×#call-by
2 ×#data type
2 ×#morphism

TLCA-1999-Andreoli #coordination

The Coordination Language Facility and Applications (JMA), pp. 1–5.

TLCA-1999-EidorffHMNST #approach #problem

AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem (PHE, FH, CM, HN, MHS, MT), pp. 6–13.

TLCA-1999-Abrusci #logic

Modules in Non-communicative Logic (VMA), pp. 14–24.

TLCA-1999-BaillotP #complexity #geometry #interactive

Elementary Complexity and Geometry of Interaction (PB, MP), pp. 25–39.

TLCA-1999-BarreiroE #revisited #semantics

Quantitative Semantics Revisited (NB, TE), pp. 40–53.

TLCA-1999-Berardid

Total Functionals and Well-Founded Strategies (SB, Ud), pp. 54–68.

TLCA-1999-BrodaD

Counting a Type’s Principal Inhabitants (SB, LD), pp. 69–82.

TLCA-1999-Damiani #algebra #data type #detection

Useless-Code Detection and Elimination for PCF with Algebraic Data types (FD), pp. 83–97.

TLCA-1999-David

Every Unsolvable λ Term has a Decoration (RD), pp. 98–113.

TLCA-1999-GianantonioFH #game studies #semantics #λ-calculus

Game Semantics for Untyped λβη-Calculus (PDG, GF, FH), pp. 114–128.

TLCA-1999-DybjerS #axiom #finite #recursion

A Finite Axiomatization of Inductive-Recursive Definitions (PD, AS), pp. 129–146.

TLCA-1999-FioreS #logic

λ Definability with Sums via Grothendieck Logical Relations (MPF, AKS), pp. 147–161.

TLCA-1999-Fujita #call-by #morphism #polymorphism #λ-calculus #μ-calculus

Explicitly Typed λμ-Calculus for Polymorphism an Call-by-Value (KeF), pp. 162–176.

TLCA-1999-Goguen #framework #logic #semantics

Soundness of the Logical Framework for Its Typed Operational Semantics (HG), pp. 177–197.

TLCA-1999-Hasegawa #linear #logic

Logical Predicates for Intuitionistic Linear Type Theories (MH), pp. 198–212.

TLCA-1999-Laurent

Polarized Proof-Nets: Proof-Nets for LC (OL), pp. 213–227.

TLCA-1999-Levy #call-by #named #paradigm

Call-by-Push-Value: A Subsuming Paradigm (PBL), pp. 228–242.

TLCA-1999-MikamiA #automaton #case study #linear

A Study of Abramsky’s Linear Chemical Abstract Machine (SM, YA), pp. 243–257.

TLCA-1999-OHearn #λ-calculus

Resource Interpretations, Bunched Implications and the αλ-Calculus (PWO), pp. 258–279.

TLCA-1999-Ohori #compilation #execution #morphism

A Curry-Howard Isomorphism for Compilation and Program Execution (AO), pp. 280–294.

TLCA-1999-PolakowP #deduction #linear #logic

Natural Deduction for Intuitionistic Non-communicative Linear Logic (JP, FP), pp. 295–309.

TLCA-1999-PollZ #data type #logic

A Logic for Abstract Data Types as Existential Types (EP, JZ), pp. 310–324.

TLCA-1999-Ritter #termination

Characterising Explicit Substitutions which Preserve Termination (ER), pp. 325–339.

TLCA-1999-SatoSB

Explicit Environments (MS, TS, RMB), pp. 340–354.

TLCA-1999-Statman #consistency #equation #theorem

Consequences of Jacopini’s Theorem: Consistent Equalities and Equations (RS), pp. 355–364.

TLCA-1999-UrbanB #logic #normalisation

Strong Normalisation of Cut-Elimination in Classical Logic (CU, GMB), pp. 365–380.

TLCA-1999-Zwanenburg #type system

Pure Type Systems with Subtyping (JZ), pp. 381–396.