Jacques Fleuriot - University of Edinburgh

Jacques Fleuriot
Are you Jacques Fleuriot?

Claim your profile, edit publications, add additional information:

Contact Details

Name
Jacques Fleuriot
Affiliation
University of Edinburgh
City
Edinburgh
Country
United Kingdom

Pubs By Year

Pub Categories

 
Computer Science - Logic in Computer Science (5)
 
Computer Science - Networking and Internet Architecture (1)
 
Physics - Physics and Society (1)
 
Computer Science - Artificial Intelligence (1)
 
Computer Science - Programming Languages (1)

Publications Authored By Jacques Fleuriot

We present a marriage of functional and structured imperative programming that embeds in pure lambda calculus. We describe how we implement the core of this language in a monadic DSL which is structurally equivalent to our intended source language and which, when evaluated, generates pure lambda terms in continuation-passing-style. Read More

Suppose we have been sold on the idea that formalised proofs in an LCF system should resemble their written counterparts, and so consist of formulas that only provide signposts for a fully verified proof. To be practical, most of the fully elaborated verification must then be done by way of general purpose proof procedures. Now if these are the only procedures we implement outside the kernel of logical rules, what does the theorem prover look like? We give our account, working from scratch in the ProofPeer theorem prover, making observations about this new setting along the way. Read More

We introduce a novel parsing concept called local lexing. It integrates the classically separated stages of lexing and parsing by allowing lexing to be dependent upon the parsing progress and by providing a simple mechanism for constraining lexical ambiguity. This makes it possible for language design to be composable not only at the level of context-free grammars, but also at the lexical level. Read More

We identify the main actors in the Isabelle and Coq communities and describe how they affect and influence their peers. This work explores selected foundations of social networking analysis that we expect to be useful in the context of the ProofPeer project, which is developing a new model for interactive theorem proving based on collaboration and social interactions. Read More

We define the concept of collaborative theorem proving and outline our plan to make it a reality. We believe that a successful implementation of collaborative theorem proving is a necessary prerequisite for the formal verification of large systems. Read More

We present a rigorous framework for the composition of Web Services within a higher order logic theorem prover. Our approach is based on the proofs-as-processes paradigm that enables inference rules of Classical Linear Logic (CLL) to be translated into pi-calculus processes. In this setting, composition is achieved by representing available web services as CLL sentences, proving the requested composite service as a conjecture, and then extracting the constructed pi-calculus term from the proof. Read More