View Proposal
-
Proposer
-
Marko Doko
-
Title
-
Formalising the computational model of Human Resource Machine
-
Goal
-
-
Description
- Human Resource Machine [1] is a puzzle game which presents you with a simple programming model and asks you to solve various puzzles by developing simple programs using the given programming language.
The goal of this project is to give a precise formal definition of the computational model of Human Resource Machine, state that definition in an assisted theorem prover (e.g., Rocq [2]), then state and prove some properties about the system.
[1] https://tomorrowcorporation.com/humanresourcemachine
[2] https://rocq-prover.org/
- Resources
-
-
Background
-
-
Url
-
-
Difficulty Level
-
Easy
-
Ethical Approval
-
None
-
Number Of Students
-
0
-
Supervisor
-
Marko Doko
-
Keywords
-
-
Degrees
-