Phil Scott

Phil Scott
Are you Phil Scott?

Claim your profile, edit publications, add additional information:

Contact Details

Phil Scott

Pubs By Year

Pub Categories

Computer Science - Logic in Computer Science (4)
Physics - Physics and Society (1)
Computer Science - Programming Languages (1)
Computer Science - Artificial Intelligence (1)

Publications Authored By Phil Scott

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