Rafael Castro's user avatar
Rafael Castro's user avatar
Rafael Castro's user avatar
Rafael Castro
  • Member for 9 years, 6 months
  • Last seen more than a month ago
22 votes
1 answer
2k views

Is possible to prove undecidability of the halting problem in Coq?

8 votes
5 answers
2k views

Relationship between formal system and formal languages

8 votes
1 answer
284 views

Relation between Type Assignment system (TA) and Hindley-Milner system

6 votes
0 answers
488 views

How are observational equivalence, contextual equivalence, and extensional equality related?

4 votes
1 answer
328 views

Typing rule for binding groups

3 votes
1 answer
679 views

The law of excluded middle and decidability

2 votes
0 answers
155 views

Proving that the failure of algorithm W implies that the program is not typable

2 votes
1 answer
189 views

Construct a proof tree in Hindley-Milner with function overload

1 vote
1 answer
262 views

Comparison Procedure in Robinson's Unification Algorithm

1 vote
1 answer
2k views

Proof that L(M) = {accepts the string 1100 } is undecidable

1 vote
2 answers
330 views

Trying to understand the proof of the halting problem presented in Sipser textbook

1 vote
1 answer
90 views

Distributed predicate computation on event stream

0 votes
1 answer
111 views

If the language $A$ is decidable and the language $B$ is recognizable, then the language $A \cap B$ is recognizable?