Commit d634fb90 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents a0700894 63faa569
......@@ -98,7 +98,8 @@ The thesis is available at https://pnwamk.github.io/docs/dissertation.pdf
**ANSWER:**
A. Kent's approach is based on control flow. As soon as a variable is defined, it computes and remember under which constraints this variable can be in True or ~True. Typecases can only be done on variables, and the former information is used to refine the context of the then and else branchs. A new idea of A. Kent's thesis compared to previous works on occurence typing is the use of semantic types to store these constraints, and the use of an application inversion function to compute them. We also use this idea in our paper.
A. Kent's approach is based on control flow. As soon as a variable is defined, it computes and remember under which constraints this variable can be in True or ~True (Beppe: isn it rather False and ¬False?). Typecases can only be done on variables (Beppe: really???), and the former information is used to refine the context of the then and else branches. A new idea of A. Kent's thesis compared to previous works on occurence typing is the use of semantic types to store these constraints, and the use of an application inversion function to compute them. We also use these ideas in our paper.
(Beppe: where do we use it other than for False and ¬False?) (Beppe: isint (f x) on ne peut rien apprendre sur x )
However, our approach is not based on control flow. We do not store any additional information about variables except their types. Instead, our typecases can be applied to arbitrary expressions e and only at this moment we perform a *backward analysis* to refine the type of the subexpressions composing e.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment