View Proposal

---

Proposer

Marko Doko

Title

Constructing the unfold of an infinite datatype in Isabelle/HOL

Goal

Description

This project is part of a bigger research project to improve on how proofs about programming languages are done. The dual to normal, finite data types are (potentially) infinite codata types. Just like normal data types can be deconstructed with a fold, codata types are constructed with an unfold. There already exists a proof on how to construct the unfold, but it needs to be updated and generalized. There also exists an updated and generalized proof for the fold, so parts of it can be adapted for the unfold as well. You do not need to have previous experience with theorem proving, but you have to be interested in it. For more information, please contact Jan van Brügge (jsv2000@hw.ac.uk).

Resources

Background

Url

Difficulty Level

Challenging

Ethical Approval

None

Number Of Students

1

Supervisor

Marko Doko

Keywords

Degrees

Bachelor of Science in Computer Science
Bachelor of Science in Computer Systems
Bachelor of Science in Information Systems
Bachelor of Science in Software Development for Business (GA)
Master of Engineering in Software Engineering
Master of Design in Games Design and Development
Master of Science in Artificial Intelligence
Master of Science in Artificial Intelligence with SMI
Master of Science in Business Information Management
Master of Science in Computer Science for Cyber Security
Master of Science in Computer Systems Management
Master of Science in Computing (2 Years)
Master of Science in Data Science
Master of Science in Human Robot Interaction
Master of Science in Information Technology (Business)
Master of Science in Information Technology (Software Systems)
Master of Science in Network Security
Master of Science in Robotics
Master of Science in Software Engineering
Bachelor of Science in Computing Science
Bachelor of Engineering in Robotics
Bachelor of Science in Computer Science (Cyber Security)