10 Result(s)
within
Stephanie Weirich
Logics and Meanings of Programs
Software Engineering
-
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...
-
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
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...
