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