- First name:
Matt
- Last name:
Kaufmann
- Email address:
REMOVED
- Home page:
http://www.cs.utexas.edu/users/kaufmann/
- Phone number(s):
- Postal code:
- City:
Austin, TX
- Country:
USA
- Organization(s) you work for or study at
(please supply the name and city for each organization):
Advanced Micro Devices, Inc.
- Fields of interest
(e.g. computer linguistics, numerical analysis, business software,
medicine, bioinformatics):
Mechanized reasoning (automated theorem proving).
- Have you written any Lisp-related papers? If so, please supply
bibliographical references (and URL's, if possible).
Below is a list of all my publications related to automated reasoning. All of
those could be considered Lisp-related, since they all pertain to mechanized
reasoning tools written in Lisp. If you want me to pare this list down
somehow, let me know.
\longres{
A Tool for Simplifying Files of {ACL2} Definitions. In Proceedings of ACL2 Workshop 2003,
http://www.cs.utexas.edu/\-users/\-moore/\-acl2/\-workshop-2003/\-contrib/\-kaufmann/\-paper.pdf.
}
A Computational Logic for Applicative Common Lisp (with J Moore). In: A
Companion to Philosophical Logic, D. Jacquette (ed), Blackwell Publishers,
pp. 724-741, 2002.
Adding a Total Order to ACL2 (With P. Manolios). In Proceedings of ACL2 Workshop 2002,
http://www.cs.utexas.edu/\-users/\-moore/\-acl2/\-workshop-2002/\-contrib/\-manolios-kaufmann/\-
total-order.pdf.
Efficient Rewriting of Data Structures in ACL2 (With R. Sumners). In Proceedings of ACL2 Workshop
2002,
http://www.cs.utexas.edu/\-users/\-moore/\-acl2/\-workshop-2002/\-contrib/\-manolios-kaufmann/\-
total-order.pdf.
Formal Verification of Microprocessors at AMD (with Arthur~Flatau, David~F.~Reed, David~Russinoff,
Eric~Smith, and Rob~Sumners). Proceedings of Designing Correct Circuits 2002.
http://www.cs.chalmers.se/\-\~ms/DCC02/\-Slides.html.
Verification of Pipeline Circuits (with David M. Russinoff). Proceedings ACL2
Workshop 2000, Oct. 2000. Available at URL
http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/final/russinoff-kaufmann/paper.pdf.
{\em Computer-Aided Reasoning: An Approach} (with P. Manolios and J Moore).
Kluwer Academic Publishers, June, 2000.
{\em Computer-Aided Reasoning: ACL2 Case Studies} (editor, and contributed an
article; with co-editors P. Manolios and J Moore). Kluwer Academic Publishers,
June, 2000.
A Precise Description of the ACL2 Logic (with J Moore). Available
at URL http://\-www.cs.utexas.edu/\-users/\-moore/\-publications/\-km97a.ps.Z.
Structured Theory Development for a Mechanized Logic (with J Moore).
{\em Journal of Automated Reasoning} 26, no. 2 (2001) 161-203.
Non-Standard Analysis in ACL2 (with Ruben Gamboa). {\em Journal of Automated
Reasoning} 27(4), 323-351, 2001.
Verification of Year 2000 Conversion Rules Using the ACL2 Theorem
Prover. {\em Software Tools for Technology Transfer} 3, no. 1 (September
2000), 13-19.
ACL2 Support for Verification Projects. Invited talk, {\em Proc. 15th
Intl. Conf. on Automated Deduction}, ed. C. Kirchner and H. Kirchner,
Lec. Notes Artif. Intelligence 1421, Springer-Verlag, Berlin, 1998,
pp. 220--238.
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp (with J
Moore). {\em IEEE Transactions on Software Engineering 23}, no. 4, April 1997,
203--213. \longres{(Supersedes: (with J Moore) ACL2: An Industrial Strength Version
of Nqthm, In {\it Proceedings of the Eleventh Annual Conference on Computer
Assurance (COMPASS-96)}, IEEE Computer Society Press, June, 1996, 23--34.)}
ACL2 Theorems about Commercial Microprocessors (with B. Brock and J Moore). In
{\it Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96)},
Springer-Verlag, 1996, M. Srivas and A. Camilleri (eds.), November, 1996,
275--293.
A Mechanically Checked Proof of the AMD5$_K86^{TM}$
Floating-Point Division Program (with J Moore and T. Lynch). {\em
IEEE Trans. Computers} 47, no. 9 (1998), pp. 913--926.
Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the
Arithmetic-Geometric Mean Theorem (with Paolo Pecchiari). {\em Journal of
Automated Reasoning} 16, no. 1-2 (1996) 181-222.
Design Goals for ACL2 (with J Strother Moore), in proceedings of: {\em Third
International School and Symposium on Formal Techniques in Real Time and Fault
Tolerant Systems}, Kiel, Germany (1994), pp. 92-117. Published by
Christian-Albrechts-Universitat.
The Boyer-Moore Theorem Prover and Its Interactive Enhancement (with Robert S.
Boyer and J Strother Moore), {\em Computers and Mathematics with
Applications,} Vol. 29, No. 2, pp. 27-62, 1995.
An Extension of the Boyer-Moore Theorem Prover to Support First-Order
Quantification, {\em Journal of Automated Reasoning}, Vol. 9, No. 3.,
December 1992, pp. 355-372.
The Role of Automated Reasoningin Integrated System Verification
Environments (with Donald I. Good and J Moore), {\em Proceedings of TTCP
XTP-1 Workshop on Effective Use of Automated Reasoning Technology in
System Development}, Naval Research Laboratory, Washington DC, April
6-7, 1992.
Should We Begin a Standardization Process for Interface Logics? (with
J Moore), {\em Proceedings of TTCP XTP-1 Workshop on Effective Use of
Automated Reasoning Technology in System Development}, Naval Research
Laboratory, Washington DC, April 6-7, 1992.
An Informal Discussion of Issues in Mechanically-assisted Reasoning. (A
keynote address) in: {\em Proceedings of the 1991 International Workshop on
the HOL Theorem Proving System and its Applications}.
Functional Instantiation in First Order Logic (with Robert S. Boyer,
David M. Goldschlag, and J Strother Moore), in: {\em Artificial
Intelligence and Mathematical Theory of Computation: Papers in Honor
of John McCarthy,} Academic Press, 1991, pp. 7 - 26.
Generalization in the Presence of Free Variables: a
Mechanically-Checked Correctness Proof for One Algorithm. {\em Journal
of Automated Reasoning} 7(1991), pp. 109-158.
The Boyer-Moore Prover and Nuprl: An Experimental Comparison (with
David Basin). In: {\em Proceedings of the First Workshop on
``Logical Frameworks''}, Antibes, France, May 1990.
Demo of the Boyer-Moore Theorem Prover and some of its extensions.
In: Proceedings of the First Workshop on ``Logical Frameworks''
(informal proceedings for Esprit Basic Research Action workshop),
Antibes, France, May 1990.
An interactive enhancement to the Boyer-Moore Theorem Prover. In: {\em
Proc. 9th Intl. Conf. on Automated Deduction} (CADE-9, Argonne, Illinois, 23-26
May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin,
1988, pp. 735-736.
Comparing Specification Paradigms for Secure Systems: Gypsy and the
Boyer-Moore Logic (with William Young), in: {\em Proceedings of the 10th
National Computer Security Conference (1987)}.
- Have you developed or participated in the development of any
Lisp-related programs or libraries? If so, please supply a URL,
if possible.
ACL2: http://www.cs.utexas.edu/users/moore/acl2/
Pc-Nqthm: http://www.computationallogic.com/software/pc-nqthm/index.html
- Lisp variants you have used (e.g. Common Lisp, Scheme, Dylan):
Common Lisp.
- Lisp variants you're currently using or intend to use in the
near future:
Common Lisp.
- Lisp implementations you have used
(e.g. CMUCL, Lispworks, Allegro Common Lisp):
GCL, Allegro CL, CMUCL, CLISP, Lispworks, MCL, OpenMCL.
- Lisp implementations you're currently using or intend to use
in the near future:
GCL, Allegro CL, CMUCL, CLISP, Lispworks, MCL, OpenMCL.
- Computer platforms on which you're using or deploying Lisp:
x86, Sun/Solaris, MacOS.
- Number of years of experience with Lisp:
20.
- Do you use Lisp:
- at work (if so, how much)
Several hours a week.
- for study (if so, how much)
- as a hobby (if so, how much)
- Are you using Lisp as much as you would like to?
If not, why not?
- Do you see any obstacles to further Lisp growth (if so, what
is the biggest obstacle in your opinion)?
- Would you be interested in a Lisp-related job or contract work?
Probably not at this time.
- Is your organization interested in hiring Lisp programmers?
Not at this time.
- Are you currently participating in Lisp-related meetings?
If so, where and how often?
If not, would you be interested in such meetings?
Not at this time.
- Do you know any other Lispers who might be willing to fill in
this questionnaire (please supply their email-address if you
do)?