Stuart F. Allen  
(sfa@cs.cornell.edu)

Few persons care to study logic, because everybody conceives himself
to be proficient enough in the art of reasoning already. But I observe that
this satisfaction is limited to one's own ratiocination, and does not extend
to that of other men. (C.S. Peirce, "The Fixation of Belief", 1877)
Everybody uses the scientific method about a great many things and only
ceases to use it when he does not know how to apply it. (same source)
People like mental pictures; they give them something to do besides just listening.
(David Sedaris)
Give a man a fish and you feed him for a day. Beat him senseless with a
fish and one fish is enough for a lifetime. (unquoted)
Basic Concepts and Methods
for Mathematical Expression in
the Computational Type Theory of Nuprl
(emblematic theorems)
Some Formal Math Pages (Nuprl)
Prototype Discrete Math Materials on Counting.
Some theorems about Type Cardinality.
examples: (ABC) ~ ((AB)C) ; () ~ ; (() ~ ) ; (ab) ~ (ab) ; (k inj k) ~ (k!) (a inj b) ~ (b((a1) inj (b1))) ; {x:{x:A P(x) } Q(x) } ~ {x:A P(x) & Q(x) }
Some Typeset Material.
Abstract identifiers, intertextual reference and a computational basis for recordkeeping (HTML)
Reflecting HigherOrder Abstract Syntax in Nuprl (10pp), with Eli Barzilay (for TPHOLs'02, track B, work in progress)
Justifying Calculational Logic by a Conventional Metalinguistic Semantics, TR991771 (25pp), with Rick Aaron, Cornell
From dy/dx to [ ]P: a matter of notation, a paper (9pp) presented in Eindhoven at the 1998 conference on User Interfaces for theorem provers. (UITP'98  link broken by Eindhoven)
The Semantics of Reflected Proof (LICS 1990, corrections 1998) (15pp, postscript)
Some informal companion notes on applying Loeb's method.A NonTypeTheoretic Definition of MartinLof's Types. LICS 1987, TR87932(16pp), Cornell
A NonTypeTheoretic Semantics For TypeTheoretic Language. Thesis, TR87866(130pp), Cornell
Redux of What's the Matter with Kansas?
Handy postscript catalog of latex mathsymbols, basic and amssymb.
latex math symbs.ps
latex math symbsCOMPACT.ps(compressed into 2 pages).
Tarski's Result about Truth predicates not
representing themselves.
Eli Barzilay's formalization of the proof is available
(on local web only for now) both in
Barzilay's
preferred notation and in the
Alternative
notation used in the orginal informal proof.
A Paradigm for Material Implication.
Some other links of interest to me.
MyhillNerode Library Improvements (planned)
Nuprl Google Searches Some Searches (local) that found the PRL site.
Some diagrams of lemma dependency in Nuprl theory int_2: int 2 thms.ps int 2 thms about division1 sfa.ps
FDL notes
Progress note (local)
on FDL Conceptual Basis June 2002.
(Lori and Christoph reduced it to a
couple of paragraphs (local)
for inclusion in a report.)
Integer Square Root Loop Example
Level Variable Extraction (local)
Files indicating ML tactics mentioned in proofs of STD nuprl4 lib: TacticUsageFREQ.txt, TacticUsageALPHA.txt, TacticUsageExamples.txt.
Nuprl/html_file_count_report.txt
Nuprl/html_file_count_reportOBS.txt
PVS/Libraries/html_file_count_report.txt
Last (4/19/0) cs786 I gave was Universes.
GPS waypoints around Cornell and Ithaca.
file:///home/sfa/nuprlLatexDumps/
Depictions of Mohammed et alia