View Proposal
-
Proposer
-
Joe Wells
-
Title
-
implement constraint solving for type inference for System Fs
-
Goal
-
-
Description
- System F is a type system that is embedded as part of the essential core in type systems used by many programming language and proof
systems. The key idea of System F is the forall-quantified type, e.g., the type (forall x. x to x) stands for the collection of all types
of the shape (Z to Z) for any Z. System Fs extends System F with _expansion variables_ to enable a particular way of using constraint
solving for finding types for programs and proof skeletons with incomplete type information. This project is about implementing the key
features of System Fs and exploring possible constraint solving algorithms.
- Resources
-
-
Background
-
types, logic, constraint solving, lambda calculus
-
Url
-
-
Difficulty Level
-
Variable
-
Ethical Approval
-
None
-
Number Of Students
-
1
-
Supervisor
-
Joe Wells
-
Keywords
-
-
Degrees
-
Bachelor of Science in Computer Science
Master of Engineering in Software Engineering
Master of Science in Computing (2 Years)
Master of Science in Data Science
Master of Science in Software Engineering
Bachelor of Science in Computing Science