Tag: general

• The λ-calculus, 2: the Church-Rosser theorem (14 Oct 2024)
  
• Introduction to the λ-calculus (30 Sep 2024)
  
• The mysteries and frustrations of numerical proofs (25 Jul 2024)
  
• The End (?) of the ALEXANDRIA project (31 Aug 2023)
  
• Porting the HOL Light metric space library (12 Jul 2023)
  
• The ALEXANDRIA Project: what has been accomplished? (27 Apr 2023)
  
• On the infinite (01 Feb 2023)
  
• Thoughts on user interfaces for theorem provers (14 Dec 2022)
  
• Memories: first exposure to computers (07 Dec 2022)
  
• Verifying cryptographic protocols, II: a simple example (02 Nov 2022)
  
• Verifying cryptographic protocols, I: Fundamentals (19 Oct 2022)
  
• Verifying distributed systems with Isabelle/HOL, by Martin Kleppmann (12 Oct 2022)
  
• Memories: Edinburgh ML to Standard ML (05 Oct 2022)
  
• Memories: Edinburgh LCF, Cambridge LCF, HOL88 (28 Sep 2022)
  
• Porting libraries of mathematics between proof assistants (14 Sep 2022)
  
• A few small formalisation challenges (03 Aug 2022)
  
• Mathematical truth, mathematical modelling and axioms (27 Jul 2022)
  
• How Isabelle emerged from the trends of the 1980s (13 Jul 2022)
  
• On Turing machines (06 Jul 2022)
  
• What is the point of formalising mathematics? (22 Jun 2022)
  
• Sledgehammer: some history, some tips (13 Apr 2022)
  
• Types versus sets (and what about categories?) (16 Mar 2022)
  
• Proving the obvious (12 Jan 2022)
  
• The de Bruijn criterion vs the LCF architecture (05 Jan 2022)
  
• Do Gödel's incompleteness theorems matter? (15 Dec 2021)
  
• ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician (08 Dec 2021)
  
• On logical formalisms (27 Oct 2021)
  
• Welcome to Machine Logic! (09 Aug 2021)