Posts in the category News
Happy birthday, Dana!
 11 October 2022
 News
Today Dana Scott is celebrating the 90th birthday today. Happy birthday, Dana! I am forever grateful for your kindness and the knowledge that I received from you. I hope to pass at least a part of it onto my students.
On the occasion Steve Awodey assembled selected works by Dana Scott at CMUHoTT/scott
repository. It is an amazing collection of papers that had deep impact on logic, set theory, computation, and programming languages. I hope in the future we can extend it and possibly present it in better format.
As a special treat, I recount here the story the invention of the famous $D_\infty$ model of the untyped $\lambda$calculus. I heard it first when I was Dana's student. In 2008 I asked Dana to recount it in the form of a short interview.
→ continue reading (1 comment)Two new doctors!
 12 January 2022
 News
Within a month two of my students defended their theses: Dr. Anja Petković Komel just before Christmas, and Dr. Philipp Haselwarter just yesterday. I am very proud of them. Congratulations!
Philipp's thesis An Effective Metatheory for Type Theory has three parts:

A formulation and a study of the notion of finitary type theories and standard type theories. These are closely related to the general type theories that were developed with Peter Lumsdaine, but are tailored for implementation.

A formulation and the study of contextfree finitary type theories, which are type theories without explicit contexts. Instead, the variables are annotated with their types. Philipp shows that one can pass between the two versions of type theory.

A novel effectful metalanguage Andromeda metalanguage (AML) for proof assistants which uses algebraic effects and handlers to allow flexible interaction between a generic proof assistant and the user.
Anja's thesis Metaanalysis of type theories with an application to the design of formal proofs also has three parts:

A formulation and a study of transformations of finitary type theories with an associated category of finitary type theories.

A userextensible equality checking algorithm for standard type theories which specializes to several existing equality checking algorithms for specific type theories.

A general elaboration theorem in which the transformation of type theories are used to prove that every finitary type theory (not necessarily fully annotated) can be elaborated to a standard type theory (fully annotated one).
In addition, Philipp has done a great amount of work on implementing contextfree type theories and the effective metalanguage in Andromeda 2, and Anja implemented the generic equality checking algorithm. In the final push to get the theses out the implementation suffered a little bit and is lagging behind. I hope we can bring it up to speed and make it usable. Anja has ideas on how to implement transformations of type theories in a proof assistant.
Of course, I am very happy with the particular results, but I am even happier with the fact that Philipp and Anja made an important step in the development of type theory as a branch of mathematics and computer science: they did not study a particular type theory or a narrow family of them, as has hitherto been the norm, but dependent type theories in general. Their theses contain interesting nontrivial metatheorems that apply to large classes of type theories, and can no doubt be generalized even further. There is lots of lowhanging fruit out there.
→ continue readingEvery proof assistant: Arend
 28 April 2020
 Talks, News, Every proof assistant
For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.
→ continue reading (10 comments)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 Slovene is required.
The first PhD student will be advised by dr. Andrej Bauer. The topic of research is foundations of type theory. The candidate should have interest in mathematical aspects of type theory, and familiarity with proof assistants is desirable.
The second PhD student will be advised by dr. Matija Pretnar. The topic of research is the theory of programming languages with a focus on computational effects. The candidate should have interest in both the mathematical foundations and practical implementation of programming languages.
Candidates should send their applications as soon as possible, but no later than the end of April, to Andrej Bauer or Matija Pretnar, depending on their primary interest. Please include a short CV, academic record, and a statement of interest.
→ continue readingA postdoc position in the Effmath research project is available at the University of Ljubljana, Faculty of Mathematics and Physics. The precise topic is flexible, but should generally be aligned with the project (see project description). Possible topics include:
 reasoning about computational effects
 implementation of computational effects
 proof assistants and formalization of mathematics
The candidate should have a PhD degree in mathematics or computer science, with background knowledge relevant to the project area. The position is available for a period of one year with possibility of extension, preferably starting in early 2016. No knowledge of the Slovene language is required.
The candidates should contact Andrej Bauer by email as soon as possible, but no later than January 8th 2016. Please include a short CV and a statement of interest.
→ continue readingThe HoTT book
 20 June 2013
 Constructive math, General, Type theory, News, Publications
The HoTT book is finished!
Since spring, and even before that, I have participated in a great collaborative effort on writing a book on Homotopy Type Theory. It is finally finished and ready for public consumption. You can get the book freely at http://homotopytypetheory.org/book/. Mike Shulman has written about the contents of the book, so I am not going to repeat that here. Instead, I would like to comment on the sociotechnological aspects of making the book, and in particular about what we learned from opensource community about collaborative research.
→ continue reading (10 comments)A hott thesis
 23 August 2012
 Type theory, News, Tutorial
Egbert Rijke successfully defended his master thesis in Utrecht a couple of weeks ago. He published it on the Homotopy type theory blog (here is a direct link to the PDF file (revised)). The thesis is well written and it contains several new results, but most importantly, it is a gentle yet nontrivial introduction to homotopy type theory. If you are interested in the topic but do not know where to start, Egbert's thesis might be perfect for you. As far as I know it is the first substantial piece of text written in (informal) homotopy type theory.
What I find most amazing about the work is that Egbert does not have to pretend to be a homotopy type theorist, like us old folks. His first contact with type theory was homotopy type theory, which impressed on his mind a new kind of geometric intuition about $\Pi$'s, $\Sigma$'s and $\mathrm{Id}$'s. If we perform enough such experiments on young bright students, strange things will happen.
→ continue reading (4 comments)Matija and I are pleased to announce a new major release of the eff programming language.
In the last year or so eff has matured considerably:
 It now looks and feels like OCaml, so you won't have to learn yet another syntax.
 It has static typing with parametric polymorphism and type inference.
 Eff now clearly separates three basic concepts: effect types, effect instances, and handlers.
 How eff works is explained in our paper on Programming with Algebraic Effects and Handlers.
 We moved the source code to GitHub, so go ahead and fork it!
Bob Harper has a blog
 18 March 2011
 News, Programming
Bob Harper of CMU, has recently started a blog, called Existential Type, about programming languages. He is a leading expert in Programming Languages. I remember being deeply inspired the first time I heard him talk. I was an incoming graduate student at CMU and he presented what the programming languages people at CMU did. His posts are fun to read, unreserved and very educational. Highly recommended!
→ continue readingEuropean workshop on computational effects
 04 January 2011
 Computation, News
Alex Simpson, Matija Pretnar and I are organizing a workshop on computational effects. It will take place in Ljubljana on March 17th and 18th 2011. More information is available at the workshop web page.
→ continue readingAn amazing functional
 29 July 2010
 Computation, News
Martin Escardo and Paulo Oliva have been working on the selection monad and related functionals. The selection monad `S(X) = (X > R) > X` is a cousin of the continuation monad `C(X) = (X > R) > R` and it has a lot of useful and surprising applications. I recommend their recent paper “What Sequential Games, the Tychonoff Theorem and the DoubleNegation Shift have in Common” which they wrote for MSFP 2010 (if you visit the workshop you get to hear Martin live). They explain things via examples written in Haskell, starting off with the innocently looking functional `ox` (which i I am writting as ox
in Haskell for “crossed O”):
ox :: [(x > r) > x] > ([x] > r) > [x] ox [] p = [] ox (e : es) p = a : ox es (p . (a:)) where a = e (\x > p (x : ox es (p . (x:))))
It is just four lines of code, so how complicated could it be? Well, read the paper to find out. If you are ready for serious math, have a look at this paper instead.
→ continue reading (3 comments)After more than 1300 days of uninterrupted service, the good old PC that served the blog started to spontaneously reboot every 4 minutes or so. It looks like a hardware failure. I moved the site to a temporary machine. I am seriously considering renting a private virtual server and just forget about buying my own hardware in the future.
On top of that I discovered that evil forces planted a phishing attack on the blog about two weeks ago. The strategy was this:
 Create an account on my blog (I stupidly left registration open to everyone).
 Elevate account privileges to administrator by exploiting a WordPress security hole (I do not know which one).
 Upload evil files to the upload area.
 Direct phishing victims to the uploaded files.
So, keep your WordPress as closed as possible.
→ continue reading (3 comments)This is a short note pointing out that the recent paper on“Mathematical undecidability and quantum randomness” by Tomasz Paterek et al. is no black magic, and that the authors are well aware of it. Unfortunately the paper appeared on Slashdot and has since generated an infinite amount of quasimathematical discussions.
→ continue reading (2 comments)Exact real arithmetic in Haskell
 03 September 2008
 Computation, Guest post, News, Software
HERA is an implementation of exact real arithmetic in Haskell using the approach by Andrej Bauer and Iztok Kavkler, see these and these slides. It uses the fast multiple precision floating point library MPFR. Download source, and see documentation and examples of usage at my home page.
[Note by Andrej: this is a guest post by Aleš Bizjak, a firstyear student of mathematics at my department. I am very proud of the excellent work he did on his summer project.]
→ continue readingPaul Taylor has published a revised version of his `lambda`calculus for real analysis. I recommend it to anyone who is interested in real analysis, be it a computer scientist, numerical analyst, or just a “true” analyst.
The first, second, and third time I talked to Paul I could not understand a word of what he was saying, and that's not just because he is a native speaker of English English. I only began to “get it” when he visited me in Ljubljana. So I think it's perhaps worth explaining a bit what this “`lambda`calculus for real analysis” is about.
→ continue reading (7 comments)This year the International Mathematical Olympiad took place in Slovenia. I participated as one of the organizers (problem selection and coordination). It was probably one of the busiest and most exciting times of my life,
→ continue reading