Madrid, Spain

Computer Science Engineering student at Complutense University of Madrid (UCM). I am interested in type theory and how it can be used to make programs fast and correct.

Formalization of Mathematical Logic and Theoretical Computer Science in the Cubical Agda theorem prover

c06ebfc `Use type classes for operators`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

499cf04 `Add product constructions for DFA`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

11ba4cc `Add product constructions for DFA`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

63e6e1c `Add product constructions for DFA`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

02da137 `Add .gitignore`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

628d592 `Add closure properties of regular languages`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

edd33e4 `Implement multi-tape Turing machines`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

d02660d `Some renaming in TM`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

8edbb8c `Reimplement Turing Machines' tape as an infinite sequence of symbols`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

0bb075e `Add definition of Turing Machines`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

01bffe6 `Add TODO keyword for incomplete proofs`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

7a18f23 `Add TODO keyword for incomplete proofs`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

117d423 `Redefine IsFinite and use it as typeclass`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

6baae12 `Define pushdown finite automata`

~jorge-jbs pushed to ~jorge-jbs/theory-of-computation git

~jorge-jbs/theory-of-computation

New git repository added

1 year, 10 months ago via formalization-in-cubical-agda