The Curious Engineer

All blogs / Math

Mathematics and Computation

math.andrej.com

A blog about mathematics for computers

MathFunctional / PL theory

’00’05’10’15’20’25
Posts
216 from 1 Aug 1997 to 10 Jul 2026
Posting
now and then (2 in the last year)
Kind
personal blog
Feed
https://math.andrej.com/feed.xml

2026 2

  1. Making AI smarter with AI
  2. Claude and I

2024 1

  1. Space-filling curves, constructively

2023 7

  1. On indefinite truth values
  2. Variations on Weihrauch degrees (CiE 2023)
  3. Continuity principles and the KLST theorem
  4. Isomorphism invariance and isomorphism reflection in type theory (TYPES 2023)
  5. Formalizing invisible mathematics
  6. slides with speaker notes
  7. Exploring strange new worlds of mathematics

2022 4

  1. Happy birthday, Dana!
  2. One syntax to rule them all
  3. Is every projective setoid isomorphic to a type?
  4. Two new doctors!

2021 5

  1. The proposal for a proof assistants StackExchange site
  2. The dawn of formalized mathematics
  3. Computing an integer using a Grothendieck topos
  4. The Burali-Forti argument in HoTT/UF
  5. Synthetic mathematics with an excursion into computability theory

2020 22

  1. continue reading
  2. continue reading
  3. A general definition of dependent type theories
  4. continue reading
  5. continue reading
  6. continue reading
  7. continue reading
  8. lengthy
  9. continue reading
  10. photos of mathematicians
  11. Slides with speaker notes
  12. what-is-an-explicit-bijection.pdf
  13. CiE-2023-slides.pdf
  14. On fixed-point theorems in synthetic computability
  15. Spartan Type Theory
  16. AndromedaProofAssistant.pdf
  17. the slides with speaker notes
  18. derivations-as-computations-icfp-2019.pdf
  19. TYPES 2017 – A modular formalization of type theory in Coq
  20. slides with speaker notes
  21. demo-icfp2019.m31
  22. Every proof assistant: Arend

2019 8

  1. On fixed-point theorems in synthetic computability
  2. Runners in action
  3. On complete ordered fields
  4. The blog moved from Wordpress to Jekyll
  5. What is algebraic about algebraic effects?
  6. Derivations as computations (ICFP 2019 slides)
  7. What is an explicit bijection? (FPSAC 2019 slides)
  8. A course on homotopy (type) theory

2018 2

  1. How to implement type theory in an hour
  2. Algebraic effects and handlers at OPLSS 2018

2017 3

  1. Spartan type theory
  2. A modular formalization of type theory in Coq
  3. Two PhD positions in Ljubljana starting October 2017

2016 11

  1. Five stages of accepting constructive mathematics
  2. The new and improved Programming languages zoo
  3. Formal proofs are not just deduction steps
  4. Hask is not a category
  5. The Andromeda proof assistant (Leeds workshop slides)
  6. nat.m31
  7. universe.m31
  8. The real numbers in homotopy type theory (CCA 2016 slides)
  9. hott-reals-cca2016.pdf
  10. A Brown-Palsberg self-interpreter for Gödel's System T
  11. self-interpreter-for-T.pdf

2015 7

  1. Postdoc position in Ljubljana
  2. Agda Writer
  3. Provably considered harmful
  4. Intermediate truth values
  5. The troublesome reflection rule (TYPES 2015 slides)
  6. The troublesome reflection rule (TYPES 2015)
  7. Another PhD position in Ljubljana

2014 11

  1. A HoTT PhD position in Ljubljana
  2. project description
  3. TEDx “Zeroes”
  4. Reductions in computability theory from a constructive point of view
  5. lc2014-slides-notes.pdf
  6. Seemingly impossible constructive proofs
  7. Brazilian type checking
  8. brazilian-type-checking.pdf
  9. Intuitionistic Mathematics and Realizability in the Physical World
  10. real-world-realizability.pdf
  11. Univalent foundations subsume classical mathematics

2013 4

  1. Costa's minimal surface with PovRay
  2. The elements of an inductive type
  3. How to review formalized mathematics
  4. The HoTT book

2012 19

  1. Free variables are not “implicitly universally quantified”!
  2. How to implement dependent type theory III
  3. How to implement dependent type theory II
  4. How to implement dependent type theory I
  5. Am I a constructive mathematician?
  6. Substitution is pullback
  7. A hott thesis
  8. continue reading
  9. The pullback lemma
  10. pullback.pdf
  11. fixed-points.pdf
  12. The topology of the set of all types
  13. Programming with Algebraic Effects and Handlers
  14. Eff 3.0
  15. eff page
  16. eff.pdf
  17. A puzzle about typing
  18. On the Bourbaki-Witt Principle in Toposes
  19. Bw.pdf

2011 15

  1. Embedding the Baire space into natural numbers
  2. How to make the “impossible” functionals run even faster
  3. continue reading
  4. Video lectures as screencasts
  5. Definability and extensionality of the modulus of continuity functional
  6. Constructive gem: an injection from Baire space to natural numbers
  7. Stone Duality for Skew Boolean Algebras with Intersections
  8. Running a classical proof with choice in Agda
  9. sba.pdf
  10. Bob Harper has a blog
  11. Video tutorials for the Coq proof assistant
  12. Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions
  13. Alg
  14. European workshop on computational effects
  15. The Dialectica interpertation in Coq

2010 16

  1. continue reading
  2. Delimited continuations in eff
  3. How eff handles built-in effects
  4. previous post
  5. the second part
  6. Random Art and the Law of Rotten Software
  7. An amazing functional
  8. Hardware failure and phishing attacks
  9. Random art in Python
  10. randomart.py
  11. Proof of negation and proof by contradiction
  12. A new style for the blog
  13. Tutorial on exact real numbers in Coq
  14. Metric Spaces in Synthetic Topology
  15. effalg.pdf
  16. csms_in_synthtop.pdf

2009 15

  1. Constructive gem: irrational to the power of irrational that is rational
  2. Constructive gem: double exponentials
  3. Constructive gem: juggling exponentials
  4. cardinality of finite sets
  5. Constructive stone: minima of sets of natural numbers
  6. Constructive gems and stones
  7. finite sets
  8. Mathematically Structured but not Necessarily Functional Programming
  9. msfp2008-slides.pdf
  10. msfp2008-abstract.pdf
  11. On programming language design
  12. comment 27
  13. How to simulate booleans in simply typed lambda calculus?
  14. the Bourbaki-Witt and Knaster-Tarski fixed-point theorems in the effective topos
  15. Miniprolog

2008 19

  1. A comment about “Mathematical undecidability and quantum randomness” by Tomasz Paterek et al.
  2. A toy call-by-push-value language
  3. A Haskell monad for infinite search in finite time
  4. Not all computational effects are monads
  5. Remote Backup with Secure Shell and Rsync
  6. Sub and Poly, two new additions to the PL Zoo
  7. Exact real arithmetic in Haskell
  8. Efficient computation with Dedekind reals
  9. Intuitionistic mathematics for physics
  10. slides-map2008.pdf
  11. slides-cca2008.pdf
  12. abstract-cca2098.pdf
  13. An object-oriented language Boa
  14. The Programming Languages Zoo
  15. Representations of uncomputable and uncountable sets
  16. Lambda calculus for real analysis by Paul Taylor
  17. The hydra game
  18. A constructive theory of domains suitable for implementation
  19. constructive-domains.pdf

2007 14

  1. Seemingly impossible functional programs
  2. these slides
  3. domains8-slides.pdf
  4. cca2007-slides.pdf
  5. cie2007-slides.pdf
  6. Synthetic Computability (MFPS XXIII Tutorial)
  7. Metric Spaces in Synthetic Topology
  8. 3wft.pdf
  9. Implementing real numbers with rz
  10. On a proof of Cantor's theorem
  11. rzreals.pdf
  12. cie-short.pdf
  13. cie-long.pdf
  14. RZ: a tool for bringing constructive and computable mathematics closer to programming practice

2006 8

  1. Are small sentences of Peano arithmetic decidable?
  2. International Mathematical Olympiad 2006
  3. Continuity Begets Continuity (Frauenwörth slides)
  4. continuity_begets_continuity_bavaria_slides.pdf
  5. König's Lemma and the Kleene Tree
  6. earlier post
  7. Interesting higher-order functionals
  8. Specifications via Realizability (Dagstuhl)

2005 13

  1. Design of Computer Algebra Systems
  2. First Steps in Synthetic Computability Theory (Fischbachau)
  3. Proof hacking
  4. Realizability as the Connection between Computable and Constructive Mathematics
  5. The Dedekind Reals in Abstract Stone Duality
  6. The blog has moved to math.andrej.com
  7. Blog as a repository for research papers
  8. How many is two?
  9. The Law of Excluded Middle
  10. ASCIIMathML
  11. MFPS XXI version
  12. What this blog is about
  13. “Specifications via Realizability (CLASE)”

2004 2

  1. Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability
  2. Propositions as [Types]

2002 3

  1. A Relationship between Equilogical Spaces and Type Two Effectivity
  2. Equilogical Spaces
  3. Comparing Functional Paradigms for Exact Real-number Computation

2001 1

  1. Sheaf Toposes for Realizability

2000 2

  1. The Realizability Approach to Computable Analysis and Topology
  2. Continuous Functionals of Dependent Types and Equilogical Spaces

1999 1

  1. Mixed multibasic and hypergeometric Gosper-type algorithms

1997 1

  1. Analytica — An Experiment in Combining Theorem Proving and Symbolic Computation