View Proposal
-
Proposer
-
Marko Doko
-
Title
-
Formalizing Tag Systems in Rocq
-
Goal
-
-
Description
- A tag system is a model of computation that operates on a FIFO queue. The system looks at the head of the queue, then (depending on the symbol that was at the head) appends some symbols at the end of the queue. The processing continues until either the queue is empty or the symbol at the head of the queue indicates the processing should be halted.
Take a look at the Wikipedia page for more info: https://en.wikipedia.org/wiki/Tag_system
The goal of this project is to formalise the results of the 2018 paper "Generalized Tag Systems" [1] using Rocq theorem prover [2].
[1] https://link.springer.com/chapter/10.1007/978-3-030-00250-3_8
[2] https://rocq-prover.org/
- Resources
-
-
Background
-
-
Url
-
-
Difficulty Level
-
High
-
Ethical Approval
-
None
-
Number Of Students
-
0
-
Supervisor
-
Marko Doko
-
Keywords
-
functional programming, theorem proving.
-
Degrees
-
Bachelor of Science in Computer Science
Master of Engineering in Software Engineering