Recent content in Blogs on György Kurucz's blog
The goal of this project is to cross-compile Lean programs to the ESP32-C3. (You can find all the code in this repository .) Lean is a dependently typed pure functional programming language and a proof assistant, though in this article I will mostly be using it just as a programming language. Its compiler can either emit LLVM IR or C code. I will be using the C output for simplicity, but using the…
Table Of Contents Introduction R-trees Insertion Deletion Complexity Specification Informal specification Formal specification in Coq Techniques Extraction Erasing proofs Dependent types Arithmetic Transpiling to JavaScript The sig type Coq’s #[program] attribute Termination Proving termination manually Rewriting with permutations Rewriting with morphisms Proof automation Reflection for use…
Introduction Coq is a proof assistant that lets you state and prove propositions in a kind of constructive logic, the Calculus of Inductive Constructions . The main reason for using such a system is because proofs written in it can be efficiently machine checked. Coq is built around the Coq kernel , the component responsible for checking the validity of proofs. The kernel is deliberately kept…
This article is meant to be a quick introduction to dependently typed programming, and theorem proving through the Curry–Howard isomorphism. I assume basic knowledge of programming in statically typed imperative languages, as well as familiarity with some basic concepts from first order classical logic (quantifiers, implication, conjunction, disjunction). I will be using Idris for the…
I currently am on a quest to find a generally useful functional language that I could experiment with on various projects. While this article specifically is about OCaml, I have plans for trying out other languages as well, so first I will talk in general about my criteria for evaluating functional languages. How am I evaluating functional languages I don’t consider this list to be complete…