Typed Lambda Calculi and Applications

Name: Typed Lambda Calculi and Applications | 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings

Luke Ong(Herausgeber*in)

Springer (Verlag)

Erschienen am 12. Juni 2011

XII, 245 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-21691-6 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Title
Preface
Organisation
Table of Contents
Abstracts of Invited Lectures
A Survey of Classical Realizability
References
Tree Automata, (Dis-)Equality Constraints and Term Rewriting
References
Rewriting in Practice
References
Combining Proofs and Programs
Contributed Papers
Higher-Order Dynamic Pattern Unification for Dependent Types and Records
Introduction
7005-Calculus
Constraint-Based Unification
Typing Modulo
A Higher-Order Dynamic Pattern Unification Algorithm for Dependent Types and Records
Inverting Substitutions
Pruning
Unifying Two Identical Existential Variables
Correctness
Solutions to Unification
Transitions Preserve Types
Conclusion
References
Classical Call-by-Need and Duality
The Duality of Computation
Call-by-Need and Duality
Minimal Call-by-Need in Sequent Calculus Form (mlv)
Soundness and Completeness of mlv
Minimal Call-by-Need in Natural Deduction (need)
Soundness and Completeness of need
Correspondence between mlv and need
Classical Call-by-Need in Sequent Calculus (lv) and Natural Deduction Form (need)
Dual Classical Call-by-Need in Sequent Calculus Form (ln)
Conclusions and Future Work
References
Homotopy-Theoretic Models of Type Theory
Introduction
Background on Type Theory
Logical Framework of Martin-Löf Type Theory
Type Constructors and
Background on Model Categories
Main Theorem and Examples
Groupoids
Extreme Examples
Localized Structures on (Pre)sheaf Categories
Future Research
References
Game Semantics and Uniqueness of TypeInhabitance in the Simply-Typed ?-Calculus
Introduction
Preliminaries
Simply-Typed ?-Calculus
Arenas and Typings
Games and Strategies
Strategies as Terms
Interpreting ?-Terms
Game-Theoretic Characterization of Principal Typings
Expressing Structural Properties
First-Order Copying Terms
Proof Uniqueness for Copy(1)-Terms
Conclusion
References
Orthogonality and Boolean Algebras for Deduction Modulo
Introduction
Classical Sequent Calculus Modulo
A Generalized Semantics
Behaviours
The Pre-boolean Algebra of Sequents
An Underlying Boolean Algebra
Conclusion
References
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
Introduction
Categories with Families
Definition
The Indexed Category of Types in Context
The 2-Category of Categories with Families
Pseudo Cwf-Morphisms
Pseudo Cwf-Transformations
2-Categories of Cwfs with Extra Structure
Forgetting Types and Terms
Rebuilding Types and Terms
Action on 0-Cells
Action on 1-Cells
Action on 2-Cells
Pseudofunctoriality of H
The Biequivalences
References
Realizability Proof for Normalization of Full Differential Linear Logic
Full Differential Linear Logic
Syntax
Dynamics
Realizability Tools
Observable and Duality
Behaviors in LL
Weak Normalisation of Linear Logic
Reducibility Candidates in LL
Reducibility
Weak Normalisation of Full Differential Linear Logic
Behaviors and Reducibility Candidates in Full-DiLL
Reduction of Exponential Macro-Constructions
Reducibility
References
Controlling Program Extraction in Light Logics
Types, First-Order Terms and Formulas
The Proof System
Elementary Time Characterisation
Polynomial-Time Characterisation
References
An Elementary Affine ?-Calculus with Multithreading and Side Effects
Introduction
A Modal -Calculus with Multithreading and Regions
Syntax
Operational Semantics
Depth System
Elementary Bound
An Elementary Affine Type System
Expressivity
Conclusion
References
B\"{o}hm's Theorem for Resource Lambda Calculus through Taylor Expansion
Resource Calculus
A Syntactic Characterization of Taylor Equality
Separating a Finite Term from Infinitely Many Terms
A Resource Conscious Böhm's Theorem
References
Finite Combinatory Logic with Intersection Types
Introduction
Preliminaries
Exptime-completeness of Inhabitation
Exptime Upper Bound
Subtyping
Ptime Decision Procedure for Subtyping
Inhabitation with Subtyping
References
Linear Lambda Calculus and Deep Inference
Introduction
Systems SBVr and BVr
Cut Elimination of SBVr
Linear ?-Calculus with Explicit Substitutions
Completeness and Soundness of SBVr and BVr
Conclusions and Future Work
References
Partiality, State and Dependent Types
Introduction
Hoare Types by Example
Semantics
iHTT
Implementation
Related Work
Conclusion
References
A Filter Model for the ?µ-Calculus
Introduction
The ?µ Calculus
Semantics
The Filter Domain
An Intersection Type Assignment System and Filter Model
Type Preservation from Parigot's Type System to the Intersection Type System
Conclusions and Future Work
References
Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming
Introduction
The Calculus FJ^¢
Approximation Semantics
Predicate Assignment
Linking Predicates with Semantics: The Approximation Result
Expressivity
Some Observations
Conclusions and Future Work
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken