A cheatsheet of modern C++ language and library features.

papers of Per Martin Löf

Experimental proof assistant (and architecture) for dependent linear logic

An Infinitely Large Napkin

https://openpal.github.io/TypeAndProof/

Methods in Algebra (Volume 1): A Chinese textbook on Algebra

Categorical Logic Notes

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

An open-source, customizable intermediate logic textbook

An Open Encyclopedia of Proof Systems