|
PUBLICATIONS
|
 |
Bibliographies
|
|
0
|
|
|
Book chapters
|
|
0
|
|
|
Book reviews
|
|
0
|
|
|
Books
|
|
0
|
|
|
Books, edited
|
|
0
|
|
|
Conf. papers
|
|
0
|
|
|
Conf. presentations
|
|
0
|
|
|
Conferences
|
|
0
|
|
|
Discussion groups
|
|
0
|
|
|
Grants
|
|
0
|
|
|
Journal articles
|
|
0
|
|
|
Periodicals/series
|
|
0
|
|
|
Proceedings
|
|
0
|
|
|
Proceedings, papers
|
|
0
|
|
|
Reports
|
|
0
|
|
|
Special issues
|
|
0
|
|
|
Theses
|
|
0
|
|
|
Treaties
|
|
0
|
|
|
Working papers
|
|
0
|
|
|
|
STATISTICS
|
|
Citation Rank
|
|
|
|
|
Total Citations
|
|
0 |
|
|
Publications
|
|
0 |
|
|
Rank
|
|
325022 |
|
|
Viewers
|
|
4 |
|
|
Views
|
|
705 |
|
|
|
|
|
Dr. Jim Hoover
(b. ----,
d. ----)
|
( Prev | Next )
|
|
|
|
|
POSITION(S) / JOB TITLE(S):
|
|
Associate Professor |
|
|
My work is centered around the core activity of computing science: the specification and implementation of solutions to computational problems. I am interested in constructing practical programming environments which support this end. Presently this is reflected in two main projects.
I am interested in environments for formally specifying and extracting correct programs. This work began with Mizar-C, a natural deduction proof system in which every sufficiently constructive proof of a proposition like for all x-exists y such that Post[x,y], allows us to implicitly extract a function f such that for all x holds Post[x,f(x)]. This f is guaranteed to correctly implement the specifications: Given an input x produce an output y that satisfies Post[x,y]. We are moving towards a richer proof environment, full Mizar, in which we hope to resolve a major problem with implicit methods: the extracted program is hidden from the user and is not conveniently available for further reasoning.
We are also working on application frameworks tailored to the engineering domain - tools for engineers professionally responsible for their use. Our frameworks support the construction of tool families that are consistent in behaviour, do not hide their inner workings, provide for verification of computations, are auditable, and can be extended by the engineer. This work is in conjunction with industrial partners.
|
|
|
Associate Professor |
|
Computing Science |
|
University of Alberta |
|
|
Only Visible to Members of getCITED
|
|
|
Doctorate
|
|
|
University of Texas at Arlington
|
|
|
Male / English
|
|
|
Unknown |
|
|
1107-2048
(Last changed on
2003/04/27 19:30:49)
|
|
|
|
|
|
|