ECOOP 2022
Mon 6 June - Thu 7 July 2022 Berlin, Germany
Thu 30 Jun 2022 17:15 - 17:45 at Zoom - VCOOP 8 Chair(s): Tijs van der Storm

Languages with polymorphic type systems are made convenient to use by employing type inference to avoid redundant type information. Unfortunately, features such as impredicative types and subtyping make complete type inference very challenging or impossible to realize. Thus some partial type inference methods are needed.

This paper presents a form of partial type inference called \emph{elementary type inference}. Elementary type inference adopts the idea of inferring only monotypes from past work on predicative higher-ranked polymorphism. This idea is extended with the addition of explicit type applications that work for any polytypes. Thus easy (predicative) instantiations can be inferred, while all other (impredicative) instantiations are always possible with explicit type applications without any compromise in expressiveness. Our target is a System F extension with top and bottom types, similar to the language employed by Pierce and Turner in their seminal work on local type inference. We show a sound, complete and decidable type system for a calculus called $F_{<:}^e$, that targets that extension of System F. A key design choice in $F_{<:}^e$ is to consider top and bottom types as polytypes only. An important technical challenge is that the combination of predicative implicit instantiation and impredicative explicit type applications, in the presence of standard subtyping rules, is non-trivial. Without some restrictions, key properties, such as subsumption and stability of type substitution lemmas, break. To address this problem we introduce a variant of polymorphic subtyping called \emph{stable subtyping} with some mild restrictions on implicit instantiation. All the results are mechanically formalized in the Abella theorem prover.

Thu 30 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:45 - 18:15
VCOOP 8Research Papers at Zoom
Chair(s): Tijs van der Storm CWI; University of Groningen
16:45
30m
Talk
Maniposynth: Bimodal Tangible Functional ProgrammingArtifacts Evaluated - FunctionalVCOOP 2022
Research Papers
Brian Hempel University of Chicago, Ravi Chugh University of Chicago
Pre-print Media Attached
17:15
30m
Talk
Elementary Type InferenceArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalVCOOP 2022
Research Papers
Jinxu Zhao University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
17:45
30m
Talk
Defining Corecursive Functions in Coq Using ApproximationsVCOOP 2022ECOOP 2022
Research Papers
Vlad Rusu Inria, Lille, France, David Nowak CRIStAL, CNRS & University of Lille