Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
f09a4c60
Commit
f09a4c60
authored
Sep 21, 2021
by
Mickael Laurent
Browse files
make it compile
parent
665202ce
Changes
1
Hide whitespace changes
Inline
Side-by-side
scp-reviews-2108.tex
View file @
f09a4c60
...
...
@@ -518,7 +518,7 @@ string).\]
\end{answer}
\end{itemize}
\end{enumerate}
...
...
@@ -772,7 +772,7 @@ p5,11, `intersect it with': Surely the next term $(t^+ \to\neg t)$ should be neg
p7,44, typo: `andjump'
p8,33, `
\partial
\in
[
[t
_
2]
{
]
}
': It seems likely that the codomain of
p8,33, `
$
\partial
\in
{
[
}
[
t
_
2
]
{
]
}
$
': It seems likely that the codomain of
{
[
}{
[
}
\_
{
]
}{
]
}
is a subset of
\{\cal
D
\}
. Wouldn't this prevent any
function that diverges on any argument from the domain t
\_
1 from
belonging to
{
[
}{
[
}
t1 -
\textgreater
{}
t2
{
]
}{
]
}
, for any t2? I would
...
...
@@ -788,9 +788,9 @@ each $\lambda$ can't be infinite). So maybe all that non-termination stuff
doesn't matter because all well-typed programs terminate. What do you
think?
p10,17: It would be nice if you could say something about why
{
[
}
Abs-
{
]
}
should be sound. In general, if you know that x
\in
A and (A
/~
\not
B)
\not
=
\emptyset
, then you certainly can't conclude that x
\in
\not
B.
p10,17: It would be nice if you could say something about why
$
{
[
}
Abs
-
{
]
}
$
should be sound. In general, if you know that
$
x
\in
A
$
and
$
(
A
\land
B
)
\not
=
\emptyset
$
, then you certainly can't conclude that
$
x
\in
\not
B
$
.
p16,41: If the main application of occurrence typing is dynamic
languages, how would you describe the relationship between occurrence
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment