- 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)?