alim
  • Member for 5 years, 7 months
  • Last seen more than 1 year ago
0 answers
9 votes
1k views
5 bookmarks
Barendregt's Variable Convention: what does it mean?
2 answers
7 votes
2k views
3 bookmarks
$\lambda$-calculus, is there encoding of for or while?
1 answers
6 votes
246 views
3 bookmarks
why nominal unification is a first-order unification?
1 answers
5 votes
125 views
2 bookmarks
strong reduction of $\lambda$-terms, useful?
2 answers
5 votes
157 views
2 bookmarks
Nominal unification: How this lemma is proved?
2 answers
5 votes
985 views
What is a quotient structure?
2 answers
5 votes
1k views
2 bookmarks
what is variable capture in nominal logic?
1 answers
5 votes
1k views
1 bookmarks
call by value: what is a value?
1 answers
4 votes
428 views
2 bookmarks
Some points about type checking of simply typed $\lambda$-calculus?
1 answers
4 votes
411 views
1 bookmarks
How to prove equivalence relation in this case?
1 answers
4 votes
149 views
2 bookmarks
how to prove the following is a bijection?
1 answers
4 votes
137 views
3 bookmarks
what is weak extensionality in $\lambda$-calculus?
1 answers
4 votes
89 views
1 bookmarks
How to understand these exposure algorithm rules for System F sub?
2 answers
3 votes
740 views
1 bookmarks
System f-sub, how to do type checking?
0 answers
3 votes
200 views
2 bookmarks
$\lambda$-terms equal modulo $\alpha$-renaming, is this an equivalence relation?
2 answers
3 votes
105 views
what is routine induction?
2 answers
3 votes
61 views
1 bookmarks
how to use type application rule (T-TAPP)?
3 answers
3 votes
85 views
1 bookmarks
A question about type rule
1 answers
3 votes
188 views
2 bookmarks
how type checking fails?
1 answers
2 votes
281 views
2 bookmarks
what are Structural recursion, primitive recursion, recursion combinator and recursion principles?
0 answers
2 votes
200 views
1 bookmarks
Recursive definitions, How it is done?
1 answers
2 votes
58 views
"not provable", what does this to do with unification?
1 answers
2 votes
142 views
1 bookmarks
Are these examples of unification problems?
1 answers
2 votes
285 views
1 bookmarks
ground terms in logic and $\lambda$-calculus?
1 answers
2 votes
87 views
1 bookmarks
What are these questions in the PoplMark challenge asking?
1 answers
1 votes
51 views
1 bookmarks
is this an example of nominal unification?
1 answers
1 votes
333 views
1 bookmarks
how to understand the occurrences of free variables?
0 answers
0 votes
228 views
How to uniquely determine a min-cut?
1 answers
0 votes
87 views
2 bookmarks
$\lambda x. \lambda x.x$ vs $\lambda y. \lambda x.x$
0 answers
0 votes
223 views
1 bookmarks
what is a disagreement set in nominal unification?