Data types with Negation -- some slides from a talk about how to understand data type definitions that include negation.

The talks were a while ago, but I never put the slides online anywhere.

https://bentnib.org/posts/2023-01-15-datatypes-with-negation.html

A few "recent developments in data structures that were already quite good" papers for your evening:

TEBs -- tree-encoded bitmaps (beating Roaring Bitmaps): http://www.db.in.tum.de/~lang/papers/tebs.pdf

HOTs -- height-optimized tries (beating ARTs): https://dbis.uibk.ac.at/sites/default/files/2022-04/binna_tods_2022.pdf

BloomRFs -- bloom range-filters (beating SuRFs): https://arxiv.org/pdf/2207.04789.pdf

Complementary foundations for mathematics: when do we choose? ~ Michael Shulman. https://home.sandiego.edu/~shulman/papers/jmm2022-complementary.pdf #Logic #Math

The EGRAPHS workshop will be taking place again at PLDI 2023 in Orlando! See you there!

Start thinking about a talk that will generate great discussion about anything related to e-graphs. Deadline: Apr 5

[New Blog Post] Datalog as a Theorem Prover: Harrop Formula-lite https://www.philipzucker.com/datalog-theorem-harrop/ #datalog #logic

here are my group's talks from the recent LLVM Developers Meeting!!

Zhengyang Liu presenting his superoptimizer for x86 vector code

https://www.youtube.com/watch?v=s1u_E_6_fvY

Nader Bushehri presenting our work on discovering miscompiles in the AArch64 backend by combining fuzzing and formal methods

https://www.youtube.com/watch?v=QLnPfcDNcpY

Yuyou Fan presenting his mutation engine for LLVM IR https://www.youtube.com/watch?v=TrCfvDHPrrs

Vsevolod Livinskii presenting his fuzzer for loop optimizers

https://www.youtube.com/watch?v=Yyj2Fex9yEo

new bloggies: an annotated semi-space collector https://wingolog.org/archives/2022/12/10/a-simple-semi-space-collector

Besides the fact that Andy is a delight to read, I think it's important in this day of Rust-infused reflexive dislike of GC to push back a little: a semispace GC is an incredibly elegant and simple device that neatly answers your language's entire memory management question like 75% of the time. Sure there are some limitations and taxes to pay, but they're often within reason for a given problem space, and it works great. Embrace it!

Why cubical type theory, and why cubical Agda?

The discussion in this thread is going to be a bit technical in several fronts. Sorry.

I was meaning to write this for a while, but this discussion motivated me to write this now:

https://mathstodon.xyz/@agdakx@types.pl/109479087194839726

1/

Cubical type theory was a mistake :( https://github.com/agda/agda/pull/6396#issuecomment-1343006786

An intrinsically scoped version of the LambdaPi tutorial using de Bruijn indices & levels: https://test.idris-lang.org/Idris2/papers/source/Language.IntrinsicScoping.TypeTheory.html

This is not a shitpost thank you.

A regexp is a logical formula with denotation in a set of "non standard truth values": the poset of predicates on strings rather than classical truth values {top, bot}. Empty and alternatives denote the bottom element and the join of this poset. Regular languages are closed under intersection so it is ok to add in conjunction as well. Kleene star is a particular LFP. The characters are atomic formulae and the empty string/sequencing are interpreted as a nice monoidal structure of the poset of languages (Day convolution).

A different way to say this is that regular expressions can all be interpreted as formulae in a non-symmetric variant of the logic of bunched implications where the sequencing is the *.

[New Blog Post] Groupoid Annotated Unions Finds https://www.philipzucker.com/union-find-groupoid/

ICYMI: Sebastian Ullrich (KIT) at #RacketCon

Metaprograms and Proofs: Macros in Lean 4

Something that is kinda cool is that CoDebruijin actually becomes *simpler* when we have less structural rules! For linear types we no longer need multiple thinnings for a node, a single one suffices. For *ordered* linear types we can go even further; the thinnings can be encoded by spliting indicies instead of masks.