Publication

On Fast Code Completion using Type Inhabitation

2012
Reports

Abstract

Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes and suggests valid expressions of a given type at a given program point. As the basis of our technique we use type reconstruction for lambda calculus with subtyping. We show that the inhabitation problem in the presence of subtyping remains PSPACE-complete. We introduce a succinct representation for type judgements that merges types into equivalence classes to reduce the search space. We introduce a proof rule on this succinct representation of types and show that it is sound and complete for inhabitation. We implemented the resulting algorithm and deployed it as a plugin for the Eclipse IDE for Scala.

Official source

https://infoscience.epfl.ch/entities/publication/3a51559f-0e50-407e-ae9a-42833bceb288

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

2012
Reports

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/3a51559f-0e50-407e-ae9a-42833bceb288

About this result

Related concepts (32)

Type theory

In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general, type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Most computerized proof-writing systems use a type theory for their foundation, a common one is Thierry Coquand's Calculus of Inductive Constructions.

Dependent type

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, F*, Epigram, and Idris, dependent types help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.

Type system

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

Related publications (8)

On Fast Code Completion using Type Inhabitation

Chat with Graph Search

Core MHD instabilities and their spectra in advanced tokamak regimes: ideal and resistive physics

Optimization of the Channel Fabrication Process for Suspended Microchannel Resonators Semester project report Advanced NEMS Laboratory Student Name Student Number

Spores, Formally