4th Year Computer Science project proposals

Samson Abramsky

• Henkin's World: an interactive implementation of the logic of branching quantifiers
  
• A Games Workbench
  
• Bounded Set Theory as a programming language for Web-like databases
  
• An Interactive Tool for the Graphical Calculus
  

Stephen Cameron

• Robot Sheepdog
  
• Object-Oriented Splines Library
  

Stephen Clark

• Statistical Natural Language Parsing
  
• Information Retrieval
  
• Machine Learning
  
• Artificial Intelligence
  

Bob Coecke

• Quantum Computing and Quantum Information
  
• Category Theory in Computing Science
  

Georg Gottlob

• Programming with Alternation
  

Jotun Hein and other members from Department of Statistics

• Bioinformatics Projects
  

Pete Jeavons (see also Bioinformatics projects offered by Jotun Hein's group

• Bioinformatics
  
• Computational Biology
  
• Constraint Satisfaction Problems
  

Roberto Lopez

• Comparative study of Aspect Oriented Modelling techniques to support Software Product Lines
  
• Automatic code generation of Feature Oriented programs in .NET
  

Gavin Lowe

• Case studies with CSP and FDR
  
• Case studies with probabilistic CSP
  
• Synthesis of security protocols
  
• Analysis of Security Protocols
  

Andrew Martin

• Information Hiding
  
• Trusted Infrastructure for the Campus Grid
  

Tom Melham

• Mechanised Reasoning
  
• Formal Hardware Verification
  
• Machine-assisted Verification of Software
  
• Implementation of Logics
  

Oege de Moor

• Optimising run-time compilation
  
• Projects in the Programming Tools Group
  

Luke Ong

• Verifying Concurrent Programs Using LTL
  
• Deciding Equivalence of Deterministic Pushdown Automata
  
• Termination Analysis of Lambda Calculus
  
• Higher Order Matching
  
• Higher Order term trees and their MSO theories
  
• Semantics of Programming Languages
  
• Types, Proofs and Categorical Logic
  
• Game Semantics and Linear Logic
  
• Foundational Structures for Concurrency
  
• Lambda Calculus
  

Joel Ouaknine

• Games and Puzzles
  
• Model Checking
  
• Timed Automata
  
• Probabilistic Systems
  
• Chess playing program (or other games)
  
• Satisfiability solvers, sudoku and other puzzles
  

Mike Spivey

• JIT translator for Oberon
  
• A debugger for Oberon
  
• Type-checking for GeomLab
  
• Bytecode for GeomLab
  
• A linear programming assistant
  

Bernard Sufrin

• Projects connected with Obol
  
• Concurrent, Distributed, and Mobile Obol
  
• Improving the efficiency of Obol with a minimalist type system
  
• Simplifying Web Application Programming
  
• Web 2.0, AJAX, Static typing
  
• From Visicale to Excel to Logicalc
  
• A Web content-management system
  
• Improving proof support in NotJape
  
• Concurrent Programming Lanuages
  
• ECSP
  
• CSP-OCCAM style Concurrency in Scala
  
• Scala/CSP.NET: Distributed Progrmming in Scala/CSP