Subscribe: Mathematics and Computation
http://math.andrej.com/feed
Preview: Mathematics and Computation

Mathematics and Computation



Mathematics for computers



Last Build Date: Mon, 29 May 2017 15:01:43 +0000

 



A modular formalization of type theory in Coq

Mon, 29 May 2017 15:01:43 +0000

Here are the slides for the talk I just gave at TYPES 2017 in Budapest. It is joint work with Philipp Haselwarter and Théo Winterhalter. The abstract for the talk is available online. It describes a complete formalization of dependent type theory which allows you to turn various features of type theory on and off, … Continue reading A modular formalization of type theory in Coq



Two PhD positions in Ljubljana starting October 2017

Tue, 28 Mar 2017 11:27:59 +0000

We are looking for two PhD students at the Faculty of Mathematics and Physics, University of Ljubljana. The programme starts in October 2017 and lasts three years. The positions will be fully funded (subject to approval by the funding agency). The candidates should have a Master’s degree in mathematics or computer science. No knowledge of … Continue reading Two PhD positions in Ljubljana starting October 2017



Five stages of accepting constructive mathematics

Mon, 10 Oct 2016 15:27:59 +0000

In 2013 I gave a talk about constructive mathematics “Five stages of accepting constructive mathematics” (video) at the Institute for Advanced Study. I turned the talk into a paper, polished it up a bit, added things here and there, and finally it has now been published in the Bulletin of the American Mathematical Society. It is … Continue reading Five stages of accepting constructive mathematics



The new and improved Programming languages zoo

Wed, 07 Sep 2016 08:39:16 +0000

It is my pleasure to announce the new and improved Programming languages Zoo, a potpourri of miniature but fully functioning programming language implementations. The new zoo has a decent web site, it is now hosted on GitHub, and the source code was cleaned up. Many thanks to Matija Pretnar for all the work. The purpose of … Continue reading The new and improved Programming languages zoo



Formal proofs are not just deduction steps

Tue, 30 Aug 2016 15:08:36 +0000

I have participated in a couple of lengthy discussions about formal proofs. I realized that an old misconception is creeping in. Let me expose it. In traditional mathematical logic (by which I mean first-order logic, as established by Hilbert, Ackermann, Skolem, Gödel and others) the concepts of logical formula and formal proof are the central notions. This … Continue reading Formal proofs are not just deduction steps