As www.lambdassociates.org says, after Spring of 2007, I will be
looking for collaboration with an institution with research interests
in any of the following areas. Collaboration includes visiting and/or
joint applications with funding and publications.
Development of Qi/tk
__________________
Qi/tk will be a complete integrated functional programming environment
with a sophisticated type secure graphical interface and a skinnable
program development environment for users to personalise to their own
requirements. It will support web programming and multiple threads
under several different Lisp platforms. You will have either an
interest in such an environment or some interest in putting it to use
in research or teaching. See www.lambdassociates.org for a preview of
Qi/tk.
GENERA for the C21
__________________
For those of you priviliged to remember the GENERA OS of the Symbolics
Lisp machine, I am interested in the C21 version. My approach will be
to develop a functional type secure OS based around Qi/tk and a Linux
kernel. Essentially this will involve transplanting Qi/tk onto a Linux
OS and using it as a shell language. The methodology will be to slowly
usurp most of the Linux commands by Qi/tk versions, whittling it down,
until what is left is a small kernel of Linux primitives coded in the
native OS language and Qi/tk providing much of the windowing and shell
language. You will definitely be a Linux geek for this project. Note
that this system should eventually be transparent w.r.t. the OS, so
that it should work under Windows too.
Intelligent Reasoning Programs
__________________________
This research thread began with some private experiments of my own in
1992 and finished with a Ph.D dissertation in 1998.
Essentially the goal was to produce an evolving reasoning system which
could adaptively improve its performance by observation of human
beings. The domain was automated reasoning and the system was designed
to be generic over different logical systems. The system was designed
to work with sequent-based systems - a very general class of systems
that can represent many formal systems. The work is fairly easily
generalised to production systems.
The modus operandus was to use evolutionary machine learning techniques
to evolve problem-solving strategies which were assessed by their
acccuracy in reflecting the original patterns of problem-solving. My
1992 paper dealt with this and raised some unsolved problems which were
dealt with by a refinement and extension of the algorithm P0 by my
student Lopes for his Ph.D. The resulting algorithm was P1.
P1 dealt successfully with logic problems in several domains and
actually outperformed a hand-written theorem-prover for intuitionistic
propositional calculus in 1997. There was also an improved successor
P1*.
P1* was designed to work with the problem of how to get machines to
learn to reason effectively over different logics. Qi was designed to
represent different logics. Hence Qi and P1* were designed to be
together - P1* sitting inside Qi.
This research was dropped due the impossibility of getting funding in
the UK, but I want to carry this research forward. I'll be putting up
more detail about this work in the next few weeks.
Safety Critical Software and Formal Verification
_______________________________________
This includes the novel use of powerful type theories and reasoning
programs to enable the production of reliable software. For a preview
of the sort of application that is possible in Qi, see studies #1, #2
and #7 in the studies in Qi series
(www.lambdassociates.org/studies/index.htm).
This is a short list and by no means exhaustive. Contact me through my
website.
Mark Tarver
dr.mtarver AT ukonline.co.uk
www.lambdassociates.org