NDLI: Is sound gradual typing dead?

Please wait, while we are loading the content...

Programming the world of uncertain things (keynote)

Breaking through the normalization barrier: a self-interpreter for f-omega

Temporal verification of higher-order functional programs

Query-guided maximum satisfiability

Fully-abstract compilation by approximate back-translation

Decidability of inferring inductive invariants

Dependent types and multi-monadic effects in F*

Automatic patch generation by learning correct code

Chapar: certified causally consistent distributed key-value stores

Principal type inference for GADTs

Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis

SMO: an integrated approach to intra-array and inter-array storage optimization

Effects as sessions, sessions as effects

Modelling the ARMv8 architecture, operationally: concurrency and ISA

Newtonian program analysis via tensor product

Lattice-theoretic progress measures and coalgebraic model checking

Learning programs from noisy data

Synthesis of reactive controllers for hybrid systems (keynote)

Type theory in type theory using quotient inductive types

Scaling network verification using symmetry and surgery

String solving with word equations and transducers: towards a logic for analysing mutation XSS

Lightweight verification of separate compilation

The hardness of data packing

Fabular: regression formulas as probabilistic programming

Estimating types in binaries using predictive modeling

'Cause I'm strong enough: Reasoning about consistency choices in distributed systems

Abstracting gradual typing

Abstraction refinement guided by a learnt probabilistic model

PolyCheck: dynamic verification of iteration space transformations on affine programs

Monitors and blame assignment for higher-order session types

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

Casper: an efficient approach to call trace collection

Algorithms for algebraic path properties in concurrent systems of constant treewidth components

Optimizing synthesis with metasketches

Confluences in programming languages research (keynote)

System f-omega with equirecursive types for datatype-generic programming

Model checking for symbolic-heap separation logic with inductive predicates

Symbolic computation of differential equivalences

From MinX to MinC: semantics-driven decompilation of recursive datatypes

The complexity of interaction

Kleenex: compiling nondeterministic transducers to deterministic streaming transducers

Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs

A program logic for concurrent objects under fair scheduling

The gradualizer: a methodology and algorithm for generating gradual type systems

Learning invariants using decision trees and implication counterexamples

Printing floating-point numbers: a faster, always correct method

Environmental bisimulations for probabilistic higher-order languages

Overhauling SC atomics in C11 and OpenCL

Pushdown control-flow analysis for free

Memoryful geometry of Interaction II: recursion and adequacy

Maximal specification synthesis

A theory of effects and resources: adjunction models and polarised calculi

Reducing crash recoverability to reachability

Unboundedness and downward closures of higher-order pushdown automata

Sound type-dependent syntactic language extension

Transforming spreadsheet data types using examples

PSync: a partially synchronous language for fault-tolerant distributed algorithms

Is sound gradual typing dead?

Symbolic abstract data type inference

Taming release-acquire consistency

Binding as sets of scopes

Example-directed synthesis: a type-theoretic interpretation

Is sound gradual typing dead?

Content Provider	ACM Digital Library
Author	New, Max S. Felleisen, Matthias Takikawa, Asumu Feltey, Daniel Greenman, Ben Vitek, Jan
Abstract	Programmers have come to embrace dynamically-typed languages for prototyping and delivering large and complex systems. When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. In response, researchers have explored the idea of gradually-typed programming languages which allow the incremental addition of type annotations to software written in one of these untyped languages. Some of these new, hybrid languages insert run-time checks at the boundary between typed and untyped code to establish type soundness for the overall system. With sound gradual typing, programmers can rely on the language implementation to provide meaningful error messages when type invariants are violated. While most research on sound gradual typing remains theoretical, the few emerging implementations suffer from performance overheads due to these checks. None of the publications on this topic comes with a comprehensive performance evaluation. Worse, a few report disastrous numbers. In response, this paper proposes a method for evaluating the performance of gradually-typed programming languages. The method hinges on exploring the space of partial conversions from untyped to typed. For each benchmark, the performance of the different versions is reported in a synthetic metric that associates runtime overhead to conversion effort. The paper reports on the results of applying the method to Typed Racket, a mature implementation of sound gradual typing, using a suite of real-world programs of various sizes and complexities. Based on these results the paper concludes that, given the current state of implementation technologies, sound gradual typing faces significant challenges. Conversely, it raises the question of how implementations could reduce the overheads associated with soundness and how tools could be used to steer programmers clear from pathological cases. .
Starting Page	456
Ending Page	468
Page Count	13
File Format	PDF
ISBN	9781450335492
DOI	10.1145/2837614.2837630
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2016-01-11
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Performance evaluation Gradual typing
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Is sound gradual typing dead?

act * AEC Is Sound Gradual Typing Dead?

Confined gradual typing

Tackling the efficiency problem of gradual typing

Design and evaluation of gradual typing for python

Abstracting gradual typing

Gradual typing for generics

Method Lookup Simulation with a Gradual Typing Language

Application optimization when using gradual typing

Is sound gradual typing dead?

Similar Documents

Is sound gradual typing dead?

act * AEC Is Sound Gradual Typing Dead?

Confined gradual typing

Tackling the efficiency problem of gradual typing

Design and evaluation of gradual typing for python

Abstracting gradual typing

Gradual typing for generics

Method Lookup Simulation with a Gradual Typing Language

Application optimization when using gradual typing

Is sound gradual typing dead?