Welcome

I am a mathematician and computer scientist who studies formalized mathematics, higher-order automated reasoning, semantics of higher-order logic, and logical frameworks. I obtained my Ph.D. in 2004 from the Department of Mathematical Sciences at Carnegie Mellon University.

I am currently employed as a scientific researcher in the programming systems group of Professor Gert Smolka at Universität des Saarlandes in Saarbrücken, Germany, funded by SFB 378.

My work website is here.
My work phone number is 681-302-5340.
Work Email:

For personal emails or emails related to this web site:

Book

Chad E Brown Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church's Type Theory College Publications. Studies in Logic: Logic and Cognitive Systems, volume 10. 2007

Papers

Published and Unpublished Material Written by Chad E. Brown

Slides

Slides from some of my talks.

Scunak

Scunak : Scunak is a Mathematical Assistant System I wrote in 2005 and 2006. Scunak is based on set theory encoded in a dependent type theory with proof irrelevance. Scunak 1.0 is coded in lisp and can run under Allegro Common Lisp or clisp.

SEMHOL Course

SEMHOL Course Web Page Semantics of Higher-Order Logic

Landau's Grundlagen

Information about translated versions of the Jutting-Automath Encoding of Landau's book Grundlagen der Analysis.

Fun with Irrational Square Roots

JSIRSRPNLO: The JavaScript (Ir)rationality of Square Roots Prover with Natural Language Output Try this...Just enter 2 and push the button. (Make sure JavaScript is enabled for your browser.) Then try 4. Please don't try negative numbers!