Index|Projects|Planet|Services

Planet

PLT, n-Categorical, and Constructive Mathematics blogs.

Sun, 29 Nov 2020 — 12:30
Generated with org-webring — v2.0.0


Dependent Type Theory as an n-Theory

No summary available.

The n-Category Café

The Uniform Measure

No summary available.

The n-Category Café

Every proof assistant: introducing homotopy.io – a proof assistant for geometrical higher category theory

After a short pause, our next talk in the series will be given by Jamie Vicary, who will present a proof assistant in which the proofs are drawn! Introducing homotopy.io: A proof assistant for geometrical higher category theory Time: Thursday, November 26, 2020 from 15:00 to 16:00 (Central European Time, UTC+1)Location: online at Zoom ID 989 0478 8985Speaker: Jamie Vicary (University of Cambridge)Proof assistant: homotopy.io Abstract: Weak higher categories can be difficult to work with algebraically, wit…

Mathematics and Computation

The Tenfold Way

No summary available.

The n-Category Café

Stellenbosch is Hiring

No summary available.

The n-Category Café

Release of Frama-C 22.0 (Titanium)

No summary available.

Frama-C RSS News

Magnitude Homology of Enriched Categories and Metric Spaces

No summary available.

The n-Category Café

Erik Palmgren Memorial Conference

Erik Palmgren, professor of Mathematical Logic at Stockholm University, passed away unexpectedly in November 2019. This conference will be an online workshop to remember and celebrate Erik’s life and work. There will be talks by Erik’s friends and colleagues, as … Continue reading →

Homotopy Type Theory

The Categorical Origins of Lebesgue Integration, Revisited

No summary available.

The n-Category Café

Octonions and the Standard Model (Part 8)

No summary available.

The n-Category Café

Octonions and the Standard Model (Part 7)

No summary available.

The n-Category Café

Questions about Questions

No summary available.

The n-Category Café

Octonions and the Standard Model (Part 6)

No summary available.

The n-Category Café

Octonions and the Standard Model (Part 5)

No summary available.

The n-Category Café

Compiling a Lisp: Labelled procedure calls

first – previous Welcome back to the Compiling a Lisp series. Last time, we learned about Intel instruction encoding. This time, we’re going to use that knowledge to compile procedure calls. The usual function expression in Lisp is a lambda — an anonymous function that can take arguments and close over variables. Procedure calls are not this. They are simpler constructs that just take arguments and return values. We’re adding procedure calls first as a stepping stone to full closure support. This will he…

Max Bernstein's Blog

Beta release of Frama-C 22.0-beta (Titanium)

No summary available.

Frama-C RSS News

Epidemiological Modeling With Structured Cospans

No summary available.

The n-Category Café

No New Normed Division Algebra Found!

No summary available.

The n-Category Café

Compiling a Lisp: Instruction encoding interlude

first – previous Welcome back to the Compiling a Lisp series. In this thrilling new update, we will learn a little bit more about x86-64 instruction encoding instead of allocating more interesting things on the heap or adding procedure calls. I am writing this interlude because I changed one register in my compiler code (kRbp to kRsp) and all hell broke loose — the resulting program was crashing, rasm2/Cutter were decoding wacky instructions when fed my binary, etc. Over the span of two very interesting …

Max Bernstein's Blog

on "binary security of webassembly"

Greets!You may have seen an interesting paper cross your radar a couple months ago: Everything Old is New Again: Binary Security of WebAssembly, by Daniel Lehmann, Johannes Kinder and Michael Pradel. The paper makes some strong claims and I would like to share some thoughts on it.reader-response theoryFor context, I have been working on web browsers for the last 8 years or so, most recently on the JavaScript and WebAssembly engine in Firefox. My work mostly consists of implementing new features, which if…

wingolog

malloc as a service

Greetings, internet! Today I have the silliest of demos for you: malloc-as-a-service.loading walloc... >  JavaScript disabled, no walloc demo. See the walloc web page for more information. // function activate_walloc_demo() { let escape = str => { return str.replace(/&/g,'&amp;').replace(/</g,'&lt;').replace(/>/g,'>'); }; let $ = document.getElementById.bind(document); let addLog = (container, html) => { let e = document.createElement(container); e.innerHTML = …

wingolog

Compiling a Lisp: Heap allocation

first – previous Welcome back to the “Compiling a Lisp” series. Last time we added support for if expressions. This time we’re going add support for basic heap allocation. Heap allocation comes in a couple of forms, but the one we care about right now is the cons primitive. Much like AST_new_pair in the compiler, cons should: allocate some space on the heap, set the car and cdr, and tag the pointer appropriately. Once we have that pair, we’ll want to poke at its data. This means we should probably also i…

Max Bernstein's Blog

Notes to self on frama-c

Frama-C is a giant modular system for writing formal proofs of C code. For months I’ve been on-and-off trying to see if we could use it to do useful proofs for any parts of the projects we write, like qemu, … Continue reading →

Richard WM Jones

Compiling a Lisp: If

first – previous Welcome back to the “Compiling a Lisp” series. Last time we added support for let expressions. This time we’re going to compile if expressions. Compiling if expressions will allow us to write code that performs decision making. For example, we can write code that does something based on the result of some imaginary function coin-flip: (if (= (coin-flip) heads) 123 456) If the call to coin-flip returns heads, then this whole if-expression will evaluate to 123. Otherwise, it will evaluate…

Max Bernstein's Blog

Finding memory leaks with Memtrace

Memory issues can be hard to track down. A function that only allocates a few small objects can cause a space leak if it’s called often enough and those objects are never collected. Even then, many objects are supposed to be long-lived. How can a tool, armed with data on allocations and their lifetimes, help sort out the expected from the suspicious?

Jane Street Tech Blog

HoTT Dissertation Fellowship

Update (Nov. 13): Application deadline extended to December 1, 2020. PhD students close to finishing their thesis are invited to apply for a Dissertation Fellowship in Homotopy Type Theory. This fellowship, generously funded by Cambridge Quantum Computing and Ilyas Khan, will provide … Continue reading →

Homotopy Type Theory

Compiling a Lisp: Let

first – previous Welcome back to the “Compiling a Lisp” series. Last time we added a reader (also known as a parser) to our compiler. This time we’re going to compile a new form: let expressions. Let expressions are a way to bind variables to values in a particular scope. For example: (let ((a 1) (b 2)) (+ a b)) Binds a to 1 and b to 2, but only for the body of the let — the rest of the S-expression — and then executes the body. This is similar to this very rough translated code in C: int result; { int …

Max Bernstein's Blog

Cast notation: a case study

I recently wrote on the SIGPLAN blog about how PL notation is a barrier to entry. While the arguments are mine, I acknowledge the many folks who helped me write it in the post. Ideas from an interesting conversation with Neel Krishnaswami came up again in a comment from Jeremy Gibbons. The universe has spoken: […]

weaselhat

Introducing parallelism in Lwt with Multicore OCaml

Lwt is OCaml’s widely used concurrency library. It offers powerful primitives for concurrent programming which have been used in many systems for effective I/O parallelism. Recently, we have been doing some experiments to add support for CPU parallelism in Lwt with Multicore OCaml. This post will showcase some ways to speed up Lwt applications with Multicore OCaml. Lwt_preemptive Lwt_preemptive module has the facility for preemptive scheduling, unlike rest of Lwt which operates in a cooperative manner. Lwt…

Sudha Parimala

New Normed Division Algebra Found!

No summary available.

The n-Category Café

Compiling a Lisp: Reader

first – previous Welcome back to the “Compiling a Lisp” series. This time I want to take a break from compiling and finally add a reader. I’m finally getting frustrated manually entering increasinly complicated ASTs, so I figure it is time. After this post, we’ll be able to type in programs like: (< (+ 1 2) (- 4 3)) and have our compiler make ASTs for us! Magic. This will also add some nice debugging tools for us. For example, imagine an interactive command line utility in which we can enter Lisp expres…

Max Bernstein's Blog

Strategic Deriving

A comprehensive guide for deriving in Haskell

Kowainik Blog

Special Numbers in Category Theory

No summary available.

The n-Category Café

Compiling a Lisp: Primitive binary functions

first – previous Welcome back to the “Compiling a Lisp” series. Last time, we added some primitive unary instructions like add1 and integer->char. This time, we’re going to add some primitive binary functions like + and <. After this post, we’ll be able to compile programs like: (< (+ 1 2) (- 4 3)) Note that these expressions may look like function calls but, like last chapter, they are not opening new stack frames (which I’ll explain more about later). Instead, the compiler will recognize that the prog…

Max Bernstein's Blog

Memory allocator showdown

Since version 4.10, OCaml offers a new best-fit memory allocator alongside its existing default, the next-fit allocator. At Jane Street, we've seen a big improvement after switching over to the new allocator. This post isn't about how the new allocator works. For that, the best source is these notes from a talk by its author. Instead, this post is about just how tricky it is to compare two allocators in a reasonable way, especially for a garbage-collected system.

Jane Street Tech Blog

A general definition of dependent type theories

The preprint version of the paper A general definition of dependent type theories has finally appeared on the arXiv! Over three years ago Peter Lumsdaine invited me to work on the topic, which I gladly accepted, and dragged my student Philipp Haselwarter into it. We set out to give an answer to the queation: What is type theory, precisely? At least for me the motivation to work on such a thankless topic came from Vladimir Voevodsky, who would ask the question to type-theoretic audiences. Some took him to…

Mathematics and Computation

Racist Bullshit in Mathematics

Robin Gandy’s “On the Axiom of Extensionality–Part 1”, Journal of Symbolic Logic, Vol. 21, No. 1 (Mar., 1956) quotes Alan Turing using a racist phrase. Yikes. Those unfamiliar with this particular racist phrase will be disappointed to learn that it’s still current enough in the UK to be used “totally unintentional[ly]”… whatever that means. Gandy’s […]

weaselhat

Every proof assistant: Cubical Agda – A Dependently Typed Programming Language with Univalence and Higher Inductive Types

I am happy to announce that we are restarting the "Every proof assistants" series of talks with Anders Mörtberg who will talk about Cubical Agda. Note that we are moving the seminar time to a more reasonable hour, at least as far as the working people in Europe are concerned. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types Time: Thursday, September 17, 2020 from 15:00 to 16:00 (Central European Summer Time, UTC+2)Location: online at Zoom ID 989 0478 8985Sp…

Mathematics and Computation

The Fall of the SKI Civilization

Abstract: The recent breakthroughs in deciphering the language and the literature left behind by the now extinct Twinklean civilization provides valuable insights into their history, science, and philosophy. The oldest documents discovered on the third planet of the star Lambda Combinatoris (also known as the Twinkle star) talk about the prehistory of the Twinklean thought. […]

  Bartosz Milewski's Programming Cafe

Compiling a Lisp: Primitive unary functions

first – previous Welcome back to the “Compiling a Lisp” series. Last time, we finished adding the rest of the constants as tagged pointer immediates. Since it’s not very useful to have only values (no way to operate on them), we’re going to add some primitive unary functions. “Primitive” means here that they are built into the compiler, so we won’t actually compile the call to an assembly procedure call. This is also called a compiler intrinsic. “Unary” means the functions will take only one argument. “F…

Max Bernstein's Blog

Compiling a Lisp: Booleans, characters, nil

first – previous Welcome back to the “Compiling a Lisp” series. Last time, we compiled integer literals. In today’s relatively short post, we’ll add the rest of the immediate types. Our programs will look like this: 'a' true false nil or () In addition, since we’re not adding too much exciting stuff today, I made writing tests a little bit easier by adding fixtures. Now, if we want, we can get a pre-made Buffer object passed into the test, and then have it destroyed afterward. Encoding Since we’re coming…

Max Bernstein's Blog

Compiling a Lisp: Integers

first – previous Welcome back to the “Compiling a Lisp” series. Last time we made a small code execution demo. Today we’re going to add the first part of our language: integer literals. Our programs will look like this: 123 -10 0 But we’re not going to put a parser in. That can come later when it gets harder to manually construct syntax trees. Also, since implementing full big number support is pretty tricky, we’re only going to support fixed-width numbers. It’s entirely possible to then implement big nu…

Max Bernstein's Blog

Announcing Signals and Threads, a new podcast from Jane Street

I’m excited (and slightly terrified) to announce that Jane Street is releasing a new podcast, called Signals and Threads, and I’m going to be the host.

Jane Street Tech Blog

Compiling a Lisp: The smallest program

previous Welcome to the first post in the “Compiling a Lisp” series. We’re going to write a small program today. Before we actually compile anything, though, let’s build up a bit of a foundation for code execution. That way, we can see the code compile and run and be satisfied with the results of both. Instead of compiling to disk, like most compilers you may be familiar with (GCC, Clang, DMD, Python, etc), we’re going to compile in memory. This means that every time we run the program we have to compile…

Max Bernstein's Blog

Compiling a Lisp: Overture

Many thanks to Kartik Agaram and Leonard Schütz for proofreading these posts. In my last series, I wrote about building a Lisp interpreter. This time, we’re going to write a Lisp compiler. This series is an adaptation of Abdulaziz Ghuloum’s excellent paper An Incremental Approach to Compiler Construction, with several key differences: Our implementation is in C, instead of Scheme Our implementation generates machine code directly, instead of generating text assembly Our implementation may omit some runtime…

Max Bernstein's Blog

Come One, Come All! The AU CS Colloquium Series is Open to All

This semester I’m the faculty chair of the AU CS Colloquium, and due to it being completely online this semester I decided to open it up to the wider community. So I’ll be doing some advertising here to get y’all to come and attend some great presentations. The complete schedule can be found here: The Colloquium Schedule Topics will vary and will include PL, category theory, security, and diversity in CS this semester. If you would like to attend please RSVP to me. The first presentation is by a NEW AU fa…

Metatheorem

What the interns have wrought, 2020 edition

It’s been an unusual internship season.

Jane Street Tech Blog

Haskell mini-patterns handbook

Collection of small Haskell patterns with detailed description, examples and exercises

Kowainik Blog

Idris 2 version 0.2.1 Released

A new version (0.2.1) of Idris 2 has been released. You can download the source (including generated Scheme and Racket files for bootstrapping) from the download page. To build it, you can either use a bootstrapping version built in Idris 1, or (the simplest way), run make bootstrap to build from the generated Scheme. Full instructions are in INSTALL.md in the distribution. Documentation is available here. To get started, you can see: Installation instructions and how to get started Changes since Idris 1 T…

Idris

What to Define When You’re Defining Gradual Type Systems

What do you have to do to define a gradual type system? You have to come up with a type system that has a question mark in it, of course. But what else?

weaselhat