You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: pages/research/index.html
+60-50
Original file line number
Diff line number
Diff line change
@@ -85,17 +85,6 @@ <h3>Conference papers</h3>
85
85
Type Inference for Rank-2 Intersection Types Using Set Unification.
86
86
ICTAC 2022.
87
87
</p>
88
-
<p>
89
-
Several type inference approaches for rank-2 idempotent and commutative intersection types have been presented in the literature.
90
-
Type inference relies on two stages: type constraint generation and solving.
91
-
Defining constraint generation rules is rather straightforward, with one exception.
92
-
To infer the type of an application, several derivations of the argument are required, one for each instance of the domain type of the function.
93
-
The types of these derivations are then constrained against the instances.
94
-
Noting that these derivations are isomorphic, by renaming of type variables, they can be obtained via a duplication operation on a single derivation of the argument.
95
-
The application rule then constrains the intersection type resulting from duplication against the domain type of the function, resulting in an equality constraint between intersections.
96
-
By treating intersections as sets, these constraints can be solved by solving a set unification problem, thus ensuring the types of the argument unify with the domain type of the function.
97
-
Here we present a new type inference algorithm for rank-2 intersection types, which relies on set unification to solve equality constraints between intersections, and show it is both sound and complete.
A Typed Lambda Calculus with Gradual Intersection Types.
201
189
PPDP 2022.
202
190
</p>
203
-
<p>
204
-
Intersection types have the power to type expressions which are all of many different types.
205
-
Gradual types combine type checking at both compile-time and run-time.
206
-
Here we combine these two approaches in a new typed calculus that harness both of their strengths.
207
-
We incorporate these two contributions in a single typed calculus and define an operational semantics with type cast annotations.
208
-
We also prove several crucial properties of the type system, namely that types are preserved during compilation and evaluation, and that the refined criteria for gradual typing holds.
Intersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their strengths. We incorporate these two contributions in a single typed calculus and define an operational semantics with type cast annotations. We also prove several crucial properties of the type system, namely that types are preserved during compilation and evaluation, and that the refined criteria for gradual typing holds.
Type Inference for Rank 2 Gradual Intersection Types.
296
294
TFP 2019.
297
295
</p>
298
-
<p>
299
-
In this paper, we extend a rank 2 intersection type system with gradual types.
300
-
We then show that the problem of finding a principal typing for a lambda term, in a rank 2 gradual intersection type system is decidable.
301
-
We present a type inference algorithm which builds the principal typing of a term through the generation of type constraints which are solved by a new extended unification algorithm constructing the most general unifier for rank 2 gradual intersection types.
In this paper, we extend a rank 2 intersection type system with gradual types. We then show that the problem of finding a principal typing for a lambda term, in a rank 2 gradual intersection type system is decidable. We present a type inference algorithm which builds the principal typing of a term through the generation of type constraints which are solved by a new extended unification algorithm constructing the most general unifier for rank 2 gradual intersection types.
0 commit comments