Linked e-resources
Details
Table of Contents
Intro
Preface
Organization
Contents
Types
Compilation Semantics for a Programming Language with Versions
1 Introduction
2 Overview
2.1 Motivating Example
2.2 VL
2.3 Programming with Versions in VL
3 Compilation
3.1 An Intermediate Language, VLMini
3.2 Girard's Translation for VLMini
3.3 Bundling
4 Algorithmic Type Inference
4.1 Pattern Type Synthesis
4.2 Type Synthesis
4.3 Extensions
5 Implementation
6 Case Study and Evaluation
6.1 Case Study
6.2 Scalability of Constraint Resolution
7 Related Work, Future Work, and Conclusion
References
What Types Are Needed for Typing Dynamic Objects? A Python-Based Empirical Study
1 Introduction
2 Background
2.1 Dynamic Object Behaviors in Python
2.2 Existing Studies on Dynamic Behaviors
3 Types for Dynamic Objects
3.1 Class-Based Types
3.2 Object-Based Types
4 Experimental Design
4.1 Subjects
4.2 Tracing and Analysis Infrastructure
5 Results and Analysis
5.1 Prevalence of Dynamic Behaviors
5.2 Effectiveness of the Types
6 Conclusion and Future Work
References
Types and Semantics for Extensible Data Types
1 Introduction
1.1 Contributions
2 Programming with Extensible Data Types, by Example
2.1 Modular Interpreters in the Style of Data Types ̀‰la Carte
2.2 Modular Algebraic Effects Using the Free Monad
2.3 Modular Higher-Order Effects
3 The Calculus
3.1 Well-Formed Types
3.2 Well-Typed Terms
3.3 Type Equivalence
4 Categorical Semantics
4.1 Semantic Setup
4.2 Interpreting Types and Type Schemes
4.3 Interpreting Arrow Types
4.4 Interpreting Terms
5 Operational Semantics
5.1 Reduction Rules
5.2 Relation to the Denotational Model
6 Related Work
7 Conclusion and Future Work
References
Functional Languages
A Diamond Machine for Strong Evaluation
1 Introduction
2 Normal Forms and the Importance of Being External
3 Preliminaries: Abstract Machines
4 Preliminaries: The Milner Abstract Machine
5 The External Abstract Machine
6 Runs to Evaluations
6.1 Leftmost Runs to Leftmost Evaluations
7 Evaluations to Runs
8 Further Pool Templates
9 Conclusions
References
Proofs as Terms, Terms as Graphs
1 Introduction
2 Preliminaries: The Focused Proof System LJF and Synthetic Inference Rules
3 The positive -calculus
4 A Graphical Representation for Terms: lambda-graphs with bodies
5 Sigma-lambda-graphs with bodies and Sigma-terms
6 Substitution and Reduction on -graphs with bodies
7 Generalization
8 Conclusion
References
Typed Non-determinism in Functional and Concurrent Calculi
1 Introduction
2 A Typed Pi-calculus with Non-deterministic Choice
2.1 Syntax and Semantics
2.2 Resource Control for spi+ via Session Types
3 A Non-deterministic Resource Lambda-calculus
Preface
Organization
Contents
Types
Compilation Semantics for a Programming Language with Versions
1 Introduction
2 Overview
2.1 Motivating Example
2.2 VL
2.3 Programming with Versions in VL
3 Compilation
3.1 An Intermediate Language, VLMini
3.2 Girard's Translation for VLMini
3.3 Bundling
4 Algorithmic Type Inference
4.1 Pattern Type Synthesis
4.2 Type Synthesis
4.3 Extensions
5 Implementation
6 Case Study and Evaluation
6.1 Case Study
6.2 Scalability of Constraint Resolution
7 Related Work, Future Work, and Conclusion
References
What Types Are Needed for Typing Dynamic Objects? A Python-Based Empirical Study
1 Introduction
2 Background
2.1 Dynamic Object Behaviors in Python
2.2 Existing Studies on Dynamic Behaviors
3 Types for Dynamic Objects
3.1 Class-Based Types
3.2 Object-Based Types
4 Experimental Design
4.1 Subjects
4.2 Tracing and Analysis Infrastructure
5 Results and Analysis
5.1 Prevalence of Dynamic Behaviors
5.2 Effectiveness of the Types
6 Conclusion and Future Work
References
Types and Semantics for Extensible Data Types
1 Introduction
1.1 Contributions
2 Programming with Extensible Data Types, by Example
2.1 Modular Interpreters in the Style of Data Types ̀‰la Carte
2.2 Modular Algebraic Effects Using the Free Monad
2.3 Modular Higher-Order Effects
3 The Calculus
3.1 Well-Formed Types
3.2 Well-Typed Terms
3.3 Type Equivalence
4 Categorical Semantics
4.1 Semantic Setup
4.2 Interpreting Types and Type Schemes
4.3 Interpreting Arrow Types
4.4 Interpreting Terms
5 Operational Semantics
5.1 Reduction Rules
5.2 Relation to the Denotational Model
6 Related Work
7 Conclusion and Future Work
References
Functional Languages
A Diamond Machine for Strong Evaluation
1 Introduction
2 Normal Forms and the Importance of Being External
3 Preliminaries: Abstract Machines
4 Preliminaries: The Milner Abstract Machine
5 The External Abstract Machine
6 Runs to Evaluations
6.1 Leftmost Runs to Leftmost Evaluations
7 Evaluations to Runs
8 Further Pool Templates
9 Conclusions
References
Proofs as Terms, Terms as Graphs
1 Introduction
2 Preliminaries: The Focused Proof System LJF and Synthetic Inference Rules
3 The positive -calculus
4 A Graphical Representation for Terms: lambda-graphs with bodies
5 Sigma-lambda-graphs with bodies and Sigma-terms
6 Substitution and Reduction on -graphs with bodies
7 Generalization
8 Conclusion
References
Typed Non-determinism in Functional and Concurrent Calculi
1 Introduction
2 A Typed Pi-calculus with Non-deterministic Choice
2.1 Syntax and Semantics
2.2 Resource Control for spi+ via Session Types
3 A Non-deterministic Resource Lambda-calculus