Some of my papers and related work

Groebner Basis Construction Algorithms Based on Superposition Loops Joint with Dr. Leonardo de Moura, Microsoft Research and Dr. Paul Jackson, LFCS, Edinburgh. In submission (2010). Abstract: We present novel Groebner basis algorithms based on saturation loops used by modern superposition theorem provers. By combining (i) top-level Groebner basis construction strategies based on the OTTER and DISCOUNT saturation loops, and (ii) sophisticated term indexing techniques derived both from ATP literature and from superfluous S-polynomial criteria in Groebner basis theory, we are able to compute Groebner bases for large, largely linear nonlinear systems of polynomial equations which are beyond the reach of previously available methods. These types of systems are typical of those arising from the use of SMT solvers in reasoning about industrial-strength software artifacts with nonlinear arithmetical components. Proving the correctness of these new Groebner basis procedures is nontrivial, and to do so we utilise the recently introduced theory of Abstract Groebner Bases. We illustrate the practical value of the algorithms through an experimental implementation within the Z3 SMT solver.	pdf (draft)
Superfluous S-polynomials in Strategy-Independent Groebner Bases Joint with Dr. Leonardo de Moura, Microsoft Research. SYNASC-2009 (11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing). IEEE Computer Society Conference Publishing Series. © IEEE (2009). Abstract: Using the machinery of proof orders originally introduced by Bachmair and Dershowitz in the context of canonical equational proofs, we give an abstract, strategy-independent presentation of Groebner basis procedures and prove the correctness of two classical criteria for recognising superfluous S-polynomials, Buchberger's criteria 1 and 2, w.r.t. arbitrary fair and correct basis construction strategies. To do so, we develop a general method for proving the strategy-independent correctness of superfluous S-polynomial criteria which seems to be quite powerful. We also derive a new superfluous S-polynomial criterion which is a generalisation of Buchberger-1 and is proved to be correct strategy-independently. Note: Until my Ph.D. thesis is complete, this paper is the best foundational reference for the theory of Abstract (a.k.a. `strategy-independent') Groebner Bases.	pdf
On Locally Minimal Nullstellensatz Proofs Joint with Dr. Leonardo de Moura, Microsoft Research. SMT-2009 (Satisfiability Modulo Theories; co-located with CADE-22). ACM International Conference Proceedings Series (ISBN 978-1-60558-484-3). © ACM (2009). Abstract: Hilbert's weak Nullstellensatz guarantees the existence of algebraic proof objects certifying the unsatisfiability of systems of polynomial equations not satisfiable over any algebraically closed field. Such proof objects take the form of ideal membership identities and can be found algorithmically using Groebner bases and cofactor-based linear algebra techniques. However, these proof objects may contain redundant information: a proper subset of the equational assumptions used in these proofs may be sufficient to derive the unsatisfiability of the original polynomial system. For using Nullstellensatz techniques in SMT-based decision methods, a minimal proof object is often desired. With this in mind, we introduce a notion of locally minimal Nullstellensatz proofs and give ideal-theoretic algorithms for their construction.	pdf
Universality of Polynomial Positivity and a Variant of Hilbert's 17th Problem Joint with Dr. Leonardo de Moura, Microsoft Research. ADDCT-2009 (Automated Deduction: Decidability, Complexity, Tractability; co-located with CADE-22) in work in progress tract. ADDCT-2009 Proceedings (2009). Abstract: We observe that the decision problem for the existential theory of real closed fields (RCF) is simply reducible to the decision problem for RCF over a connective-free universal language in which the only relation symbol is a strict inequality. In particular, every existential RCF sentence phi can be settled by deciding a proposition of the form ``polynomial p (which is a sum of squares) takes on strictly positive values over the reals,'' with p simply derived from phi. Motivated by this observation, we pose the goal of isolating a syntactic criterion characterising the positive definite (i.e., strictly positive) real polynomials. Such a criterion would be a strictly positive analogue to the fact that every positive semidefinite (i.e., non-negative) real polynomial is a sum of squares of rational functions, as established by Artin's positive solution to Hilbert's 17th Problem. We then prove that every positive definite real polynomial is a ratio of a Real Nullstellensatz witness and a positive definite real polynomial. Finally, we conjecture that every positive definite real polynomial is a product of ratios of Real Nullstellensatz witnesses and examine an interesting ramification of this conjecture.	pdf
Combined Decision Techniques for the Existential Theory of the Reals Joint with Dr. Paul Jackson, LFCS, Edinburgh. Calculemus-2009 (16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning). Lecture Notes in Artificial Intelligence (LNCS/LNAI 5625). © Springer-Verlag (2009). Abstract: Methods for deciding quantifier-free non-linear arithmetical conjectures over \mathbb{R} are crucial in the formal verification of many real-world systems and in formalised mathematics. While non-linear (rational function) arithmetic over \mathbb{R} is decidable, it is fundamentally infeasible: any general decision method for this problem is worst-case exponential in the dimension (number of variables) of the formula being analysed. This is unfortunate, as many practical applications of real algebraic decision methods require reasoning about high-dimensional conjectures. Despite their inherent infeasibility, a number of different decision methods have been developed, most of which have ``sweet spots'' -- e.g., types of problems for which they perform much better than they do in general. Such ``sweet spots'' can in many cases be heuristically combined to solve problems that are out of reach of the individual decision methods when used in isolation. RAHD (``Real Algebra in High Dimensions'') is a theorem prover that works to combine a collection of real algebraic decision methods in ways that exploit their respective ``sweet-spots.'' We discuss high-level mathematical and design aspects of RAHD and illustrate its use on a number of examples.	pdf
Proving SPARK Verification Conditions with SMT Solvers Joint with Dr. Paul Jackson, LFCS, Edinburgh. In submission (2009-2010). Abstract: We have constructed a tool for using SMT (SAT Modulo Theories) solvers to discharge verification conditions (VCs) from programs written in the SPARK language. The tool can drive any solver supporting the SMT-LIB standard input language and has API interfaces for some solvers. SPARK is a subset of Ada used primarily in high-integrity systems in the aerospace, defence, rail and security industries. Formal verification of SPARK programs is supported by tools produced by the UK company Praxis High Integrity Systems. We report in this paper on our experience in proving SPARK VCs using the popular SMT solvers CVC3, Yices, Z3 and Simplify. We find that the SMT solvers can prove virtually all the VCs that are discharged by Praxis's prover, and sometimes more. Average run-times of the fastest SMT solvers are observed to be roughly 1-2x that of the Praxis prover. Significant work is sometimes needed in translating VCs into a form suitable for input to the SMT solvers. A major part of the paper is devoted to a detailed presentation of the translations we implement.	pdf (draft)
A Survey of Sums of Squares Positivstellensatzen Methods in Real Algebraic Geometry In preparation (2008-2010). Abstract: The discipline of real algebraic geometry centers around the study of subsets of n-dimensional Euclidean space definable by boolean combinations of polynomial equations and inequalities. As such objects, known as semialgebraic sets, arise naturally in virtually all mathematical and natural sciences, the development of sophisticated techniques for their analysis is a well-motivated problem. In this survey, we are interested in a feasible semi-decision method for the following question: Given a semialgebraic set S defined as the collection of satisfying real vectors \vec{r} \in \mathbb{R}^n with respect to some conjunctive system of polynomial equations and inequalities, is S empty? As we will see, through methods deeply rooted in Artin's solution to Hilbert's 17th Problem, Stengle's Positivstellensatzen, Gram matrix constructions for quadratic forms, and a subfield of convex optimization known as semidefinite programming, modern sums of squares techniques as developed by Choi, Lam, Harrison, Parrilo, Powers, Reznick, and W\"ormann offer a promising framework for developing a feasible solution to this important problem.
Hilbert's Tenth Problem is Solvable over \mathbb{Z} and \mathbb{Q} for Rabinowitsch Zero-dimensional Ideals In preparation (2008-2010). Abstract: Hilbert's Tenth Problem asks for a general algorithm to decide if an integral polynomial p(\vec{x}) \in \mathbb{Z}[\vec{x}] has solutions in the ring of integers. In 1970, the work of Davis, Putnam, Robinson, and Matiyasevich culminated in Matiyasevich's proof that no such algorithm can exist. But the story need not end here. One may relativise Hilbert's Tenth Problem over any computable ring, e.g. to any ring whose arithmetical operations are algorithmic. In this direction, Hilbert's Tenth Problem over \mathbb{Q} remains as an important and difficult open problem at the intersection of arithmetic algebraic geometry, algebraic number theory, and mathematical logic. We give a proof, relying in large part on an exploitation of semialgebraic quantifier elimination, that Hilbert's Tenth Problem over \mathbb{Z}, \mathbb{Q}, and any algebraic number field \mathbb{Q}[\vec{\alpha}] is solvable whenever the ideal induced by the polynomial p(\vec{x}) is Rabinowitsch zero-dimensional over \mathbb{C}.
Affine Varieties and Classifying Ultrafilters In preparation (2008-2010). Abstract: We show how every affine variety can be associated with a unique ``classifying'' ultrafilter derived from the radical ideal corresponding to the variety.
Does SAT Exhibit Fractal Behavior? Joint with Dr. Joost Joosten, Institute for Logic, Language and Computation (ILLC), Univ. Amsterdam. ILLC Research Report #PP-2008-41 (2008). Abstract: In this paper we study the structure of the set SAT of all satisfiable propositional logical formulas. In particular we raise the question whether the distribution of SAT within the set A of all propositional formulas exhibits fractal behavior. This answer is of course relative to a metric on A. We show that for one such metric there is strong evidence that the distribution does indeed behave wildly. Next we look at an alternative metric.	pdf
Open Euclidean Relations and Decidable Fragments of the True Existential Theory of the Rational Number Field Abstract of BCTCS-2008 talk appears in the Bulletin of the European Association for Theoretical Computer Science (2008). Abstract: First, we call a continuous map f : \mathbb{R}^n -> \mathbb{R} a ``real-extended rational endomap'' (rcr-map) if {f(q) | q \in \mathbb{Q}^n} \subseteq \mathbb{Q}. Second, we call a binary relation R : \mathbb{R}^2 -> 2 an ``open Euclidean relation'' (oe-relation) if for all rcr-maps f, g : \mathbb{R}^n -> \mathbb{R}, {r \in \mathbb{R}^n | R(f(r), g(r))} is open in \mathbb{R}^n under the Euclidean topology. We have shown that over any first-order language L with relation symbols (R_i)_{i \in I}, function symbols (f_j)_{j \in J}, logical symbols {\exists, \and, \or}, and constant symbols (c_k)_{k \in K}, Th_L(<\mathbb{Q},(f_j)_{j \in J},(R_i)_{i \in I},(c_k)_{k \in K}>) is decidable provided that each c_k denotes a rational number and each R_i (resp. f_j ) denotes an oe-relation (resp. rcr-map) that is first-order definable in the full language of ordered rings.	pdf
A Continuous Relaxation for Proving Discrete ACL2 Theorems over Real Closed Fields Joint with Dr. Paul Jackson, LFCS, Edinburgh. Extended abstract appears in the Proceedings of TTVSI, a Festschrift in Honour of Prof. Mike Gordon FRS, The Royal Society, London, UK (2008). Abstract: The work described involves the use of a decision procedure for real closed fields (RCF) to prove theorems originally formulated with rational-valued variables in the ACL2 theorem prover. From a theoretical perspective, we have isolated an interesting nonlinear fragment of the rational number field that admits a continuous relaxation. From a practical perspective, we have used some recent additions to ACL2 aimed at interfacing with external tools to implement our procedure as a ``trusted clause-processor'' relying upon the QEPCAD-B RCF procedure as a trusted oracle.	pdf (a) pdf (p)
Diophantine Sets and Their Decision Problems Undergraduate Honors Thesis, Department of Mathematics, University of Texas at Austin. Supervised by Prof. Dr. Robert S. Boyer (2007). Abstract: We shall examine the genesis and proof of the Davis-Putnam-Robinson-Matiyasevich negative solution to Hilbert's Tenth Problem, and then proceed to prove a handful of elementary new results on definability and decidability in <\mathbb{N}, *>.	pdf
Feasible Arithmetical Proof Procedures, S.M.T., and I.B.M. 0-year Ph.D. research proposal, LFCS, University of Edinburgh (2007). Abstract: We are interested in practical proof procedures for theorems with significant number-theoretic content, and the integration of such procedures with modern Satisfiability Modulo Theories (S.M.T.) algorithms and Instance Based Methods (I.B.M.). Of particular interest is automation for proving theorems requiring non-linear arithmetic reasoning, a timely, important problem of current interest to many leaders in the field (see Paulson's ongoing EPSRC grant, Hunt et al., and Avigad-Friedman). We propose a jointly theoretical and practical focus with the following high-level goals: (1) the investigation of logical and computational aspects of decidability for fragments of arithmetic, including meta-theoretic methods for combining decision procedures for both disjoint and intersecting theories, and (2) the development of useful heuristics and semi-decision procedures for undecidable or computationally intractable fragments. For practical theorem proving, we find the recent progress of S.M.T. and I.B.M. algorithms wonderful. We believe they warrant substantial study, and we will endeavor to deliver efficient implementations of our procedural findings within state-of-the-art S.M.T. and I.B.M. systems.	pdf
Formal Verification of Graphical Programs Joint with Dr. Jacob Kornerup, National Instruments Corp. U.S. provisional patent pending (#: 6150-03400, 6150-03401) (2006).	url

Master Class in Mathematical Logic Mathematical Research Institute in the Netherlands Graduated (2007) with a research project titled ``Abstract Properties of Partial Combinatory Algebras'' Fellowship kindly endowed by DIAMANT (Discrete Interactive Algorithmic Mathematics Algebra and Number Theory, Dutch Maths. Cluster) Jointly administered by Departement Wiskunde, Universiteit Utrecht, and Subfaculteit Wiskunde der Katholieke Universiteit Nijmegen Bachelor of Arts in Mathematics with Honors University of Texas at Austin Graduated (2007) with an Honors Thesis titled ``Diophantine Sets and Their Decision Problems'' Honors Thesis advisor: Prof. Dr. Robert S. Boyer Summer (June) 2005 Guest Student Topics in Graduate Mathematics: Proof Theory University of Notre Dame, June 2005 Taught by Jeremy Avigad and Henry Towsner of C.M.U.

Game-theoretic Probability and Related Topics June 21st - 23rd, 2010 I will present a talk (joint with Yuri Gurevich) titled ``Algebraic Descriptive Randomness.'' Royal Holloway, University of London London, England, UK Scottish Theorem Proving Seminar November 20th, 2009 I presented a talk (joint with Leo de Moura) titled ``Recent Advances in SAT Modulo Nonlinear Real Arithmetic.'' University of Edinburgh, Scotland, UK SYNASC 2009 (11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing) September 26th - 29th, 2009 I presented a talk (joint with Leo de Moura) titled ``Superfluous S-polynomials in Strategy-independent Groebner Bases.'' West University, Timisoara, Romania, RISC Linz, Johannes Kepler University, Austria, and Research Institute e-Austria Timisoara Timisoara, Romania SMT 2009 (SATisfiability Modulo Theories) co-located with CADE 2009 (Conference on Autmated Deduction) August 2nd, 2009 I presented a talk (joint with Leo de Moura) titled ``On Locally Minimal Nullstellensatz Proofs.'' McGill University Quebec, Montreal, Canada ADDCT 2009 (Automated Deduction: Decidability, Complexity, Tractability) co-located with CADE 2009 (Conference on Automated Deduction) August 2nd, 2009 I presented a talk (joint with Leo de Moura) titled ``Universality of Polynomial Positivity and a Variant of Hilbert's 17th Problem.'' McGill University Quebec, Montreal, Canada Calculemus 2009: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning July 7th, 2009 I presented a talk (joint with Paul B. Jackson) titled ``Combined Decision Techniques for the Existential Theory of the Reals.'' Work appears in the book ``Intelligent Computer Mathematics'' published by Springer-Verlag. Grand Bend, Ontario, Canada MSR Internship Final Talk June 26th, 2009 I presented a talk titled ``Some Results on Nonlinear Arithmetic Helpful to Z3.'' The results covered can be found in two joint papers by Leo de Moura and myself: ``On Locally Minimal Nullstellensatz Proofs'' (in SMT-2009; pdf), ``Superfluous S-polynomials in Strategy-Independent Groebner Bases'' (in submission; pdf). Microsoft Research Redmond Redmond, WA, USA Verification Working Group April 16th, 2009 I presented a talk titled ``A High-level Sketch of the RAHD (`Real Algebra in High Dimensions') Decision Method.'' See here for an abstract of my talk. Microsoft Research Redmond Redmond, WA, USA Workshop on Linking Formal Design and Verification Tools to Create Trustworthy Software Nov 27-28th, 2008 I presented two posters (both joint with Paul Jackson): RAHD: Real Algebra in High Dimensions Improved Automation for SPARK Verification Conditions Microsoft Research Cambridge Cambridge, England, UK SRI Computer Science Laboratory Seminar October 30th, 2008 I presented a talk titled ``RAHD: A Feasible Decision Method for Real Algebra in High Dimensions.'' See here for an abstract of my talk. SRI International Menlo Park, CA, USA Summer School Marktoberdorf 2008 - Engineering Methods and Tools for Software Safety and Security August 5-17th, 2008 An Advanced Study Institute of the NATO Science for Peace and Security Programme, and The Institut für Informätik, Technische Universitat München Marktoberdorf, Germany SRI Formal Methods and Dependable Systems Group Talk I presented a talk titled ``Decision Methods for the Existential Theory of Real Closed Fields.'' June 27th, 2008 SRI International Menlo Park, CA, USA Formal Methods Outreach Workshop June 9-10th, 2008 SRI International Menlo Park, CA, USA CAMELEON - Cambridge-Leeds-Norwich Logic and Set Theory Meeting April 23rd, 2008 (a post-action shot!) I presented a talk titled ``A Family of Decidable Nonlinear Fragments of the True Existential Theory of the Rational Number Field.'' Centre for Mathematical Sciences Department of Pure Mathematics and Mathematical Statistics University of Cambridge Cambridge, England, UK BCTCS-2008 - 24th British Colloquium for Theoretical Computer Science April 7-10th, 2008 (an action shot!) I presented a talk titled ``Open Euclidean Relations and Decidable Fragments of the True Existential Theory of the Rational Number Field.'' Grey College at Durham University Banquet at Durham Castle (pretty!) Durham, England, UK TTVSI - A Festschrift in Honour of Prof. Michael J. C. Gordon FRS March 25-26th, 2008 Paul Jackson and I presented a short talk and poster on our joint work titled ``A Continuous Relaxation for Proving Discrete ACL2 Theorems over Real Closed Fields.'' The Royal Society London, England, UK IDT Talk: Edinburgh Interdisciplinary Tea Seminar March 17th, 2008 I presented a talk titled ``Isolating Decidable Nonlinear Fragments of Undecidable Number Theories.'' See here for more information. Department of Informatics University of Edinburgh Edinburgh, Scotland, UK CAMELEON - Cambridge-Leeds-Norwich Logic and Set Theory Meeting December 11th, 2007 Department of Mathematics University of East Anglia Norwich, England, UK ACL2 Theorem Prover Workshop 2007 November 15-16th, 2007 Matt Kaufmann, Jacob Kornerup, and Mark Reitblatt presented a ``Rump Session'' talk on our joint work centered around using the ACL2 theorem prover to prove properties of programs written in the graphical parallel dataflow programming language LabVIEW/G. Jeff Kodosky, the inventor of LabVIEW and founder of our theorem proving project, gave a Keynote Address on his vision for the future of our project. Note: I was sadly not able to be there in person. Co-located with FMCAD-2007 Austin, TX, USA DReaM Talk: Edinburgh Mathematical Reasoning Group October 5th, 2007 I presented a talk titled ``Hilbert's Tenth Problem and Some Weak Relatives.'' See here for an abstract of my talk. Mathematical Reasoning Group University of Edinburgh Edinburgh, Scotland, UK MAP (Mathematics: Algorithms and Proofs) January 8-12th, 2007 The Lorentz Center Universeteit Leiden Leiden, The Netherlands CAMELEON Cambridge-Leeds-Norwich Logic and Set Theory Meeting and CL Minicourse on Countable Ordinals November 29th - December 2nd, 2006 Center for Mathematical Sciences, and Computer Laboratory University of Cambridge Cambridge, England, UK PSSL-84 (Peripatetic Seminar on Sheaves and Logic) October 14-15th, 2006 Institut fur Theoretische Informatik Technical University of Braunschweig Braunschweig, Germany Association for Symbolic Logic Annual Conference Special Goedel Centennial Meeting May 17-21st, 2006 Universite du Quebec a Montreal Montreal, Quebec, Canada N.I.TECH - National Instruments Corp. Annual Technical Conference April 7th, 2006 Dr. Jacob Kornerup and I presented a talk titled ``How LabVIEW and its Theorem Prover Help You Build Absolutely Reliable Systems.'' National Instruments Corporation - Main Campus Austin, TX, USA College of Natural Sciences' Undergraduate Research Forum April 7th, 2006 I presented my work titled ``Proof Theory in Proof Theory: A Computational Relativisation of Hilbert's Program.'' Under the auspices of the Department of Computer Sciences and the Department of Mathematics College of Natural Sciences, Welch Hall Forum University of Texas at Austin Austin, TX, USA Arizona Winter School in Computational and Algorithmic Aspects of Algebra and Arithmetic March 11th-15th, 2006 Special courses in: integer factorization, explicit methods for solving Diophantine equations, computing cohomology in algebraic geometry, and discriminants, resultants, and their tropicalization. Southwestern Center for Arithmetical Algebraic Geometry University of Arizona Tucson, AZ, USA Logic for Automated Reasoning and Automated Reasoning for Logic (LARARL-2006) June 8th-12th, 2006  Cancelled I am on the programme committee. Click here for CfP. Part of The International Computer Science Symposium in Russia (CSR-2006) St. Petersburg Department of Steklov Institute of Mathematics, & Euler International Mathematical Institute St. Petersburg, Russia UT Austin ACL2 Seminar October 19th, 2005 (one day after my 22nd birthday!) I presented a talk titled "Automated Reasoning in LabVIEW with the Method/ACL2 System." A short abstract can be found here. Dept. of Computer Sciences / ACL2 Group University of Texas, Austin Austin, TX, USA Argonne Workshop on Automated Reasoning and Deduction (AWARD-2005) August 11-13, 2005 I presented a talk titled "Automated Reasoning in LabVIEW and Some Elementary Thoughts on Proof Theoretic Techniques for Automating Interpretability." Mathematics and Computer Science Division Argonne National Laboratory University of Chicago Chicago, IL, USA Topics in Graduate Mathematics: Summer Workshop in Proof Theory June 6 - June 17th, 2005 University of Notre Dame Southbend, IN, USA Group Photo! Austin Center for Advanced Studies Annual Conference April 2005 IBM Austin Center for Advanced Studies Austin, TX, USA Association for Symbolic Logic Annual Conference March 2005 Stanford University Palo Alto, CA, USA Association for Symbolic Logic Annual Conference May 2004 Carnegie Mellon University Pittsburgh, PA, USA

Oldschool Underground PC Art/BBS/Demo Scene

I am very happy to report that some of my work in the art-scene is now available as part of the Dark Domain DVD Underground Art Scene Retrospective released by ACiD Productions. This includes source code to many of my applications. I have also been told that my work in the BBS scene of the late 80s and 90s is part of both the new BBS Documentary Film (3-part series DVD) and the BBS Historical Library. I think this is very neat -- my sincere thanks go out to those who put this together! My start in mathematics and computation began with my involvement in the underground art/demo scene of the late 80s and early 90s. The scene, centered around the online bulletin board system (BBS), was a haven for artists and coders who wished to be challenged by both the limited artistic mediums of ANSI and XBiN, as well as the limitations and peculiarities of the x86 architecture when used to drive digital media. Beginning in 1995 under the handle skaboy, and working my way up towards eventually becoming head-coder for ACiD Productions, I authored numerous software packages for the art/demo scene including the Infusion Bulletin Board System, the Empathy Image Editor (source code, more info), AvengeView image viewer, AvengePackerPro art-pack manager, and Impulse Tracker Tosser. I will post links to these applications and their source code as I find them on my old hard-drives and on the internet. I am very happy to hear that Infusion is still used as the foundation of a handful of BBSs in Europe! (Which is quite surprising, since Infusion, as with many other BBS systems from those days, was negatively impacted by Y2K dating issues).

---

Music

The other half of my life is music. With my great friend Barry DeBakey, I am half of the song-writing collective Olney Clark. Our debut self-titled LP (produced by Eddy Hobizal) will be released by the Friendly Police UK label in early 2010 (here is our first music video for the album, `Josefin the writer,' directed and animated by Hanae Seida). Before this, I made a little single/ep, `Let Love Be,' released by Asian Man Records in October of 2006 (here is a music video for it), and I made a full-length record, `Brokedown Gospel,' which was released in July of 2004 by Asian Man as well, with proceeds benefitting the Plea For Peace Foundation. See the sweet folks at Asian Man Records for more. (There are also a lot of old releases from projects and bands I was in as a teenager of which I don't have copies anymore; if you do, especially Substandard's `The Complete and Total Unabridged Guide to Life, Happiness, and Humanity,' or The Record Time's `Almost Always,' then please get in touch!)

---

Memberships

The Edinburgh Mathematical Society The American Mathematical Society The Mathematical Association of America The Association for Symbolic Logic The Association for Computability in Europe The Computability and Complexity in Analysis Network The Association for Automated Reasoning The Association of Lisp Users The Association for Advancement of Artificial Intelligence Foundations of Mathematics Mailing List, NYU et al The Free Software Foundation (Associate Member) The Honors Software Development Group ACL2 Theorem Prover Group Team CL 2007

---

The mind-blowingly magical city in which I live

(Edinburgh photo by JuanJ on flickr)