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)

Contributor to the PRL Project
and the FDL Project (some FDL project Tenets and Q&A on Certificates and Design Notes and Seminar Material).

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((a-1)  inj  (b-1)))  ;  {x:{x:A| P(x)  }| Q(x) } ~ {x:A| P(x) & Q(x) }

An extra example: primes have no rational square roots.

Some Standard Nuprl Library Material.

Some Typeset Material.

Abstract identifiers, intertextual reference and a computational basis for recordkeeping (HTML)

Reflecting Higher-Order Abstract Syntax in Nuprl (10pp), with Eli Barzilay (for TPHOLs'02, track B, work in progress)

Justifying Calculational Logic by a Conventional Metalinguistic Semantics, TR99-1771 (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 Non-Type-Theoretic Definition of Martin-Lof's Types. LICS 1987, TR87-932(16pp), Cornell

A Non-Type-Theoretic Semantics For Type-Theoretic Language. Thesis, TR87-866(130pp), Cornell

Miscellaneous Links (emphasized links signify only local access)

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.

Myhill-Nerode 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.

New RecType Pages

file:///home/sfa/nuprlLatexDumps/

Whiteboard Shots

Depictions of Mohammed et alia