NDLI: Optimal inference of fields in row-polymorphic records

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

What exactly is inexact computation good for?

Taming the parallel effect zoo: extensible deterministic parallelism with LVish

Atomicity refinement for verified compilation

Surgical precision JIT compilers

First-class runtime generation of high-performance types using exotypes

Expressing and verifying probabilistic assertions

A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation

Laws of concurrent programming

Adaptive, efficient, parallel execution of parallel programs

Compiler-assisted detection of transient memory errors

On abstraction refinement for program analyses in Datalog

End-to-end verification of stack-space bounds for C programs

Commutativity race detection

Tracelet-based code search in executables

A personal perspective on concurrency

Chlorophyll: synthesis-aided compiler for low-power spatial architectures

Don't sweat the small stuff: formal verification of C code without the pain

Persistent pointer information

Improving JavaScript performance by deconstructing the type system

A lightweight symbolic virtual machine for solver-aided host languages

A model counter for constraints over unbounded strings

Test-driven repair of data races in structured parallel programs

DoubleChecker: efficient sound and precise atomicity checking

Stochastic optimization of floating-point programs with tunable precision

Getting F-bounded polymorphism into shape

Compositional solution space quantification for probabilistic software analysis

Adapton: composable, demand-driven incremental computation

Globally precise-restartable execution of parallel programs

Compiler validation via equivalence modulo inputs

Hybrid top-down and bottom-up interprocedural analysis

VeriCon: towards verifying controller programs in software-defined networks

Race detection for Android applications

Resugaring: lifting evaluation sequences through syntactic sugar

Test-driven synthesis

Natural proofs for data structure manipulation in C using separation logic

Selective context-sensitivity guided by impact pre-analysis

Doppio: breaking the browser language barrier

FlashExtract: a framework for data extraction by examples

Modular control-flow integrity

Æminium: a permission based concurrent-by-default programming language approach

Herding cats: modelling, simulation, testing, and data-mining for weak memory

A framework for enhancing data reuse via associative reordering

Optimal inference of fields in row-polymorphic records

Slicing probabilistic programs

Specialization slicing

Accurate application progress analysis for large-scale parallel debugging

Automatic runtime error repair and containment via recovery shepherding

FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps

Verification modulo versions: towards usable verification

Race detection for event-driven mobile applications

SCCharts: sequentially constructive statecharts for safety-critical applications: HW/SW-synthesis for a conservative extension of synchronous statecharts

Code completion with statistical language models

Automating formal proofs for reactive systems

Introspective analysis: context-sensitivity, across the board

Dynamic enforcement of determinism in a parallel scripting language

Consolidation of queries with user-defined functions

Dynamic space limits for Haskell

Maximal sound predictive race detection with control flow abstraction

Fast: a transducer-based language for tree manipulation

Optimal inference of fields in row-polymorphic records

Content Provider	ACM Digital Library
Author	Simon, Axel
Abstract	Flexible records are a powerful concept in type systems that form the basis of, for instance, objects in dynamically typed languages. One caveat of using flexible records is that a program may try to access a record field that does not exist. We present a type inference algorithm that checks for these runtime errors. The novelty of our algorithm is that it satisfies a clear notion of completeness: The inferred types are optimal in the sense that type annotations cannot increase the set of typeable programs. Under certain assumptions, our algorithm guarantees the following stronger property: it rejects a program if and only if it contains a path from an empty record to a field access on which the field has not been added. We derive this optimal algorithm by abstracting a semantics to types. The derived inference rules use a novel combination of type terms and Boolean functions that retains the simplicity of unification-based type inference but adds the ability of Boolean functions to express implications, thereby addressing the challenge of combining implications and types. By following our derivation method, we show how various operations such as record concatenation and branching if a field exists lead to Boolean satisfiability problems of different complexity. Analogously, we show that more expressive type systems give rise to SMT problems. On the practical side, we present an implementation of the select and update operations and give practical evidence that these are sufficient in real-world applications.
Starting Page	100
Ending Page	111
Page Count	12
File Format	PDF
ISBN	9781450327848
DOI	10.1145/2594291.2594313
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-06-09
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Type inference Boolean functions Completeness Abstract interpretation Expansion Row polymorphism
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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