Search

Hilbert's Foundations of Geometry was perhaps one of the most influential works of geometry in the 20th century and its axiomatics was the first systematic attempt to clear up the logical gaps of the Elements. But does it have gaps of its own? In this paper, we discuss a logical issue, asking how Hilbert is able to talk about natural numbers within a foundational synthetic geometry. We clarify the matter, showing how to obtain the natural numbers using a very modest subset of his axioms., Comment: 8 pages, 3 figures

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., Comment: 15 pages

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., Comment: 5 pages

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. It also makes it possible to include lightweight error-handling directly as part of the language specification instead of leaving it up to the implementation. We present a high-level algorithm for local lexing, which is an extension of Earley's algorithm. We have formally verified the correctness of our algorithm with respect to its local lexing semantics in Isabelle/HOL.

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., Comment: 15 pages, 13 figures, Research supported by EPSRC grant EP/L011794/1

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.

Within-group similarities and between-group differences are used to illustrate the socio-cultural nature of the concept-building process in highly collaborative computer science classrooms. Simultaneously, a social constructivist perspective is used to describe the individual aspects of this development. The study uses written explanations from high school students as well as novice university students to illustrate the cognitive trajectory from initial hunches to a holistic knowledge of the concepts of keys in database modelling. The main findings of the study, however, are of a general epistemological nature, as they enlighten and exemplify the social processes of these classrooms as seen from a perspective of situated cognition. Based on these findings, the paper finally addresses implications for teachers. In particular, it is emphasised that teachers need to pay careful attention to their own use of language in discursive interaction with students.

A National Curriculum for postgraduate science teacher training courses in England and Wales was first introduced in September 1999. Reviews the new curriculum and associated assessment procedures and raises points for discussion. Particular attention is paid to the implications for prospective high school physics teachers. (Author/MM)