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?

1 vote
1 answer
2k views

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

8 votes
5 answers
2k views

Relationship between formal system and formal languages

3 votes
1 answer
681 views

The law of excluded middle and decidability

6 votes
0 answers
488 views

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

1 vote
2 answers
331 views

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

4 votes
1 answer
329 views

Typing rule for binding groups

8 votes
1 answer
284 views

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

1 vote
1 answer
262 views

Comparison Procedure in Robinson's Unification Algorithm

2 votes
1 answer
189 views

Construct a proof tree in Hindley-Milner with function overload

2 votes
0 answers
155 views

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

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?

1 vote
1 answer
90 views

Distributed predicate computation on event stream