The ever-growing size of programs and their continuous evolution require building fast and efficient analyzers. Here we focus on the static ones, in particular on type systems, for both checking and inference. Just as programs change by incrementally changing or inserting pieces of code, called diffs, also type systems should be incremental and re-type the diffs, only. An algorithmic schema is proposed that mechanically derives an incremental version of existing, standard typing algorithms. Ours is a grey-box approach: just the shape of the typing rules, that of the types and some domain-specific knowledge are needed to instantiate our schema. Here, we present the foundations of our approach and the conditions for its correctness. Our schema is applied to derive four incremental typing and inference algorithms for languages in different programming paradigms. We implemented an OCaml module that inputs a type system and outputs its incrementalized version. Experimental results show that our approach is effective, and prove its usage beneficial.

Mechanical incrementalization of typing algorithms

Galletta L.
2021

Abstract

The ever-growing size of programs and their continuous evolution require building fast and efficient analyzers. Here we focus on the static ones, in particular on type systems, for both checking and inference. Just as programs change by incrementally changing or inserting pieces of code, called diffs, also type systems should be incremental and re-type the diffs, only. An algorithmic schema is proposed that mechanically derives an incremental version of existing, standard typing algorithms. Ours is a grey-box approach: just the shape of the typing rules, that of the types and some domain-specific knowledge are needed to instantiate our schema. Here, we present the foundations of our approach and the conditions for its correctness. Our schema is applied to derive four incremental typing and inference algorithms for languages in different programming paradigms. We implemented an OCaml module that inputs a type system and outputs its incrementalized version. Experimental results show that our approach is effective, and prove its usage beneficial.
Incremental typing
Program analysis
Type systems
File in questo prodotto:
File Dimensione Formato  
s2.0-S0167642321000502-main.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Nessuna licenza
Dimensione 3.85 MB
Formato Adobe PDF
3.85 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/20.500.11771/18881
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
social impact