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