Projects
Meta-CLF 2
This project applies the above methodological and technical insights obtained in the Meta-CLF project to reason about concurrent, distributed and parallel languages and systems of practical importance, such as electronic voting, web-based languages, and cryptographic protocols.- Nexcel
This project sits at the confluence of logic programming, office automation and user interface design. It studies the human impact of extending the spreadsheet paradigm with deductive reasoning capabilities.
- VirtuallySafe
This project aims to develop an integrated software and hardware approach to guaranteeing the integrity of code and data in virtual machine hypervisors. It revolves around the design of a verifiable security micro-kernel and a stream-based hypervisor integrity verifier to validate dynamic data structures.
- RIPPLE
This project explores the use of logic-based multiset rewriting as an effective approach to programming very large ensembles of distributed agents.
Older projects
- Meta-CLF
This project develops recent work on language specification with substructural operational semantics into methodologies for designing and reasoning about programming and specification languages for distributed computation.
- QWeSST
QWeSST is an exploration of the type-theoretic foundations of modern web programming, in particular remote execution, mobile code, security and persistent state, and a programming language that embodies those foundations.
- Kerberos Verification
This project embarks in a detailed specification and verification of a large commercial cryptographic protocol, Kerberos 5, thereby pushing current technology to its limit. The investigation is carried out in MSR 2.
- Deductive Spreadsheet
A deductive spreadsheet is a conservative extension of the traditional spreadsheet paradigm with a simple yet powerful, form of logical data inference.
- MSR
MSR is a family of executable specification languages based on multiset rewriting. Originally a minimal formalism for theoretical investigations, it has now evolved into a language that marries state-based and process-based descriptions of concurrent systems on sound logical foundations.
- CLF
CLF is an extension of LLF with additional operators from linear logic and a monadic construct. This type theory forms a logical framework that supports describing formalisms based on concurrency.
- LLF
LLF is a logical framework that supports encoding and reasoning about the notion of state, as found in programming languages, substructural logics, and other formalisms. At is core is a linear type theory.- MEC
MEC extends the event calculus with modalities that allow expressing that an event may eventually occur and must occur.- 'Log
'Log (pronounced quote log) is a logic programming language extended with constructs that support meta-programming, in particular a self-representation of terms and variables. - LLF
Sat 23 Oct 2010
