Programming Languages and Systems
33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part II
Page
%P
-
Book and Conference Proceedings
-
Book and Conference Proceedings
Programming Languages and Systems
33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I
-
Chapter and Conference Paper
A Dependent Dependency Calculus
Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has sh...
-
Chapter
A Reflection on Types
The ability to perform type tests at runtime blurs the line between statically-typed and dynamically-checked languages. Recent developments in Haskell’s type system allow even programs that use reflection to t...
-
Chapter and Conference Paper
Needle & Knot: Binder Boilerplate Tied Up
To lighten the burden of programming language mechanization, many approaches have been developed that tackle the substantial boilerplate which arises from variable binders. Unfortunately, the existing approach...
-
Chapter and Conference Paper
Visible Type Application
The Hindley-Milner (HM) type system automatically infers the types at which polymorphic functions are used. In HM, the inferred types are unambiguous, and every expression has a principal type. Type annotation...
-
Chapter and Conference Paper
Verified ROS-Based Deployment of Platform-Independent Control Systems
The paper considers the problem of model-based deployment of platform-independent control code on a specific platform. The approach is based on automatic generation of platform-specific glue code from an archi...
-
Article
Preface
-
Chapter and Conference Paper
Dependently-Typed Programming in GHC
Is Haskell a dependently-typed programming language?
-
Chapter
Generic Programming with Dependent Types
Some programs are doubly generic. For example, map is datatype-generic in that many different data structures support a map** operation. A generic programming language like Generic Haskell can use a single defi...
-
Chapter and Conference Paper
Combining Proofs and Programs
Programming languages based on dependent type theory promise two great advances: flexibility and security. With the type-level computation afforded by dependent types, algorithms can be more generic, as the type ...
-
Chapter
It Is Time to Mechanize Programming Language Metatheory
How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researcher...
-
Chapter and Conference Paper
Mechanized Metatheory for the Masses: The PoplMark Challenge
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?
-
Chapter and Conference Paper
Higher-Order Intensional Type Analysis
Intensional type analysis provides the ability to analyze abstracted types at run time. In this paper, we extend that ability to higherorder and kind-polymorphic type constructors. The resulting language is el...
-
Chapter and Conference Paper
Encoding Intensional Type Analysis
Languages for intensional type analysis permit ad-hoc polymorphism, or run-time analysis of types. However, such languages require complex, specialized constructs to support this operation, which hinder optimi...
-
Chapter and Conference Paper
Safe and Flexible Dynamic Linking of Native Code
We present the design and implementation of the first complete framework for flexible and safe dynamic linking of native code. Our approach extends Typed Assembly Language with a primitive for loading and type...
