Projects
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.
- 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.
- RIPPLE
This project explores the use of logic-based multiset rewriting as an effective approach to programming very large ensembles of distributed agents.
- 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.
Older projects
- 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
Saturday, 23-Oct-2010 14:02:42 AST
