~jorge-jbs

Madrid, Spain

https://jorgebs.es/

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-in-cubical-agda

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

Activity

c06ebfc Use type classes for operators

2 years ago via formalization-in-cubical-agda

499cf04 Add product constructions for DFA

2 years ago via formalization-in-cubical-agda

11ba4cc Add product constructions for DFA

2 years ago via formalization-in-cubical-agda

63e6e1c Add product constructions for DFA

2 years ago via formalization-in-cubical-agda

02da137 Add .gitignore

2 years ago via formalization-in-cubical-agda

628d592 Add closure properties of regular languages

2 years ago via formalization-in-cubical-agda

edd33e4 Implement multi-tape Turing machines

2 years ago via formalization-in-cubical-agda

d02660d Some renaming in TM

2 years ago via formalization-in-cubical-agda

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

2 years ago via formalization-in-cubical-agda

0bb075e Add definition of Turing Machines

2 years ago via formalization-in-cubical-agda

01bffe6 Add TODO keyword for incomplete proofs

2 years ago via formalization-in-cubical-agda

7a18f23 Add TODO keyword for incomplete proofs

2 years ago via formalization-in-cubical-agda

117d423 Redefine IsFinite and use it as typeclass

2 years ago via formalization-in-cubical-agda

6baae12 Define pushdown finite automata

2 years ago via formalization-in-cubical-agda
~jorge-jbs/theory-of-computation

New git repository added

2 years ago via formalization-in-cubical-agda
1 / 2