Nabla - Automated Reasoning

Jørgen Villadsen

Nabla: A Linguistic System based on Multi-dimensional Type Theory
PhD Thesis: Technical University of Denmark 1995

Project Description

The main aim of this project is to model communication protocols in automated proof tools based on higher order logic.
One application is formal verification of security protocols.

Introduction

Although this project formally started in 2004, my interest in automated reasoning and modelling based on higher order logic goes back to at least my master's thesis in 1989.

My interest in computer security and in particular communication protocols goes back to at least my employment at the Danish Defence Research Establishment (1997-1999).

I have recently participated in the Copenhagen Security Seminars, the International School on Foundations of Security Analysis and Design 2001, and the International Workshop on Foundations of Computer Security 2002 - Federated Logic Conference, Copenhagen, Denmark.

The plan for 2006 is as follows:

Publish book: Nabla: A Linguistic System based on Type Theory
Study higher order logic, notably the works by Andrews, Farmer, Gilmore, and Fitting (the latter's work is a topic of the Logic Seminars).
Verify dynamic set operations using Isabelle, with possible publication in Archive of Formal Proofs (some investigations from a student project are reported as IMFUFA 427 2003).
Evaluate the formal verification of security protocols by Paulson, for example as described in the paper: Inductive analysis of the Internet protocol TLS (Isabelle proofs).
FLoC 2006 - Federated Logic Conference, Seattle, USA (10-22 August 2006).

More ideas here: Thesis Project Proposals

Automated Reasoning and Natural Language Semantics
Talk by Patrick Blackburn at Information Seminar on the European Masters in Language and Communication Technology (Computational Linguistics, Copenhagen Business School, 14 June 2005)