Foundations of Programming Meetings
School of Computer Science and ITUniversity of Nottingham
The Foundations of Programming group holds regular research meetings. The meetings last around an hour, and are intended to be a friendly forum for discussion and exchange of ideas. Most meetings take the form of a talk by a group member or an invited speaker, but we also have various kinds of discussion sessions. The meetings are open to everyone, not just members of the group. Please contact Graham Hutton if you are interested in visiting the group and giving a talk.
Details of previous years meetings are also available: 1995; 1996; 1997; 1998; 1999; 2000; 2001; 2002. 2003.
Details of recent and upcoming meetings are given below.
Nominalism is the claim that mathematical entities---numbers, functions, sets and structures---do not exist. The nominalist faces a problem of how it is that mathematics is applied to the world. The nominalist proposal is that mathematical statements about the world can be nominalized. For example, the statement The number of Fs is at least 3 which refers to numbers can be re-expressed as There are x, y, z, all different and each an F, which refers only to things that are Fs. Here we examine such nominalizations of cardinality statements. On our method of formalizing cardinality statements and counting symbols, the nominalization of the number of Fs at least n has roughly (1/2)n3 symbols, and consequently, rather mundane cardinality claims are not, at least in practice, nominalistically expressible (at least not if we insist on the existence of relevant tokens). Second, theres a problem with cardinality explanations, in that the nominalistic computations are unfeasible. We illustrate this what might be called Pigeonhole explanations, which are in fact formalizable in first-order logic as proofs of formulas of the form PHP(m, n). But though these are theorems of first- order logic, their proofs are astronomically large, even for small values of m and n. In any case, it seems that the moral reason why a conclusion like There are at least two people in the same country is true, given the factual premises, is because the Pigeonhole Principle is true. Finally, we suggest that there may be a problem for the nominalist in asserting there are at most n objects in the world, since its austere nominalization has more than n symbols.
Paper (pdf)
I will discuss some of the relationships between context-free grammars,
class hierarchies, and algebraic types, and introduce the syntax
definition formalism EONF, a restricted form of context-free grammar
based on the ONF syntax formalism that imposes the design of
structured abstract syntax directly in the grammar. Abstract syntax
trees of better quality together with types defining their traversal
patterns and parsers can be obtained automatically for any target
language supporting parametric polymorphism, subtyping, or disjoint
sums.
We develop a simple functional language in which to explore the
semantics of synchronous exceptions and asynchronous interrupts. In
particular, we seek to define a 'finally' operator in terms of
primitives of the language, and prove that this operator has the
desired behaviour. We are not interested in whether the language is
practical for programming. This is part of a larger program of work
concerned with the semantics of the exception handling mechanisms
provided in Concurrent Haskell, and reasoning about operators and
programs written using them.
We present Timed Reasoning Logics (TRL) as a framework that allows one to
model resource-bounded reasoners. We concentrate on time-bounded reasoners,
i.e. agents that are able to produce plans or derive consequences of their
beliefs, but take time to deliberate. We can thus use TRL to model multiagent
systems over a period of time without assuming agents' beliefs to be closed
under logical consequence. TRL can thus be seen as a combination of syntactic
epistemic logics and temporal logics.
Here, we illustrate TRL concepts using a propositional natural deduction-style
reasoner, who derives consequences of its beliefs over time. Since reasoning
in natural deduction requires assumptions to be made, our model is actually a
model of a multiagent system in which assumptions are beliefs of ``helper''
agents. An agent who doesn't know whether $\phi$ can use a helper to reason
as if $\phi$ were the case; if the helper runs into a contradiction, our
first agent will believe $\neg\phi$. We show the logic used to model the
reasoner, which we call TRL(ND), is sound, complete and decidable.
In this talk, I shall introduce the main aspects of an agent-oriented
programming language and its interpreter, and then address the use of
model-checking techniques for the verification of multi-agent systems
implemented in that programming language. The first part of the talk
will cover various features of "Jason", a Java-based interpreter for
an extended version of a logic-based agent-oriented programming
language called AgentSpeak, which is based on the BDI architecture for
cognitive agents. The second part of the talk will overview the
research leading to the development of a set of tools called
CASP. These tools automatically translate AgentSpeak code and a
simplified BDI property specification language into the input
languages of existing model checkers, thus allowing the verification
of implemented (rather than high-level designs of) agent systems. To
address the state-explosion problem, abstraction techniques tailored
specifically to that agent-oriented programming language need to be
developed. Towards that, the talk will also refer to recent work on a
property-based slicing algorithm for AgentSpeak.
School of Computer Science and IT
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB
United Kingdom