Math, Logic - vpatryshev/wowiki GitHub Wiki

Logic

• Federico Aschieri, Francesco A. Genco, ⅋ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
• Bernardy, Proofs for Free
• Uli Furbach, Logic for Computer Scientists
• Valeria de Paiva, Encyclopedia
• Valeria de Paiva, Dialectica Categories
• Intro to Indian Philosophy
• Paul Downen and Zena. M. Ariola, "A Tutorial on Computational Classical Logic and the Sequent Calculus"
• Anel, "Ambiguity in Math" (video)
• John Alan Robinson, Computational Logic: Memories of the Past and Challenges for the Future
• principle of equivalence (nlab)
• P.N. Benton G.M. Biermany V.C.V. de Paiva, Computational Types from a Logical Perspective I
• Michael Stay, L.G. Meredith, Logic as a distributive law
• Kleene's T predicate Informally, the T predicate tells whether a particular computer program will halt when run with a particular input, and the corresponding U function is used to obtain the results of the computation if the program does halt.
• Rice's theorem all non-trivial, semantic properties of programs are undecidable.
• Tobias Ganzow and Lukasz Kaiser, New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures
• De Bruijn Monads
• The technical part of Godel’s proof
• Lutz Straßburger, What is a logic, and what is a proof?
• Jacobs, Categorical Logic and Type Theory (pdf), [also](https://pages.jh.edu/rrynasi1/NewFoundations4Math/Literature/Logic/Jacobs1999CategoricalLogic+TypeTheory.pdf]
• David Spivak - A summary of categorical structures in Poly
• Gödel's proof of god's existence
• A Formal Logic for Formal Category Theory
• Polynomials for Enumerable Sets... and Turing machines
• automating mathematics
• Wolfram, Where Did Combinators Come From? Hunting the Story of Moses Schönfinkel
• Probability Theory as Extended Logic
• José Alonzo, Cuaderno de Investigación en Lógica Computacional
• Куклев, Новые Основания

Toposes

• A.Joyal, Topos Theory, youtube
• Topos Colloquium online
• Barr, Wells, "Toposes, Triples and Theories"
• Topos Semantics for Higher-Order Modal Logic
• nLab, Subobject Classifier
• A.Joyal, Crash Course in Topos Theory, 1-4, youtube
• Olivia Caramello, Topos-theoretic background
• locales
• Adamek, Locally Presentable and Accessible Categories
• Laurent Lafforgue
• Johnstone, Notes on Logic and Set Theory, see it also on z-library and Anna's archive

D.Scott

• selected papers on github
• Dana S. Scott, A Timeline for Logic, λ-Calculus, and Programming Language Theory
• An Interview with Dana Scott
• D.Scott, Domains for Denotational Semantics

Model Theory

• Britannica article
• Barr, Wells, "Toposes, Triples and Theories"
• list of first order theories
• Lawvere Theories and Monads
• Vladimir Voevodsky, Lawvere theories and Jf-relative monads
• Chu. Operations and Lawvere Theories
• F.W.Lawvere page at Buffalo
• F. WILLIAM LAWVERE, FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES AND SOME ALGEBRAIC PROBLEMS IN THE CONTEXT OF FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
• Martin Hyland, John Power, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads
• algebraic data types, categorically
• [Z.L. Low, Algebraic Theories](Z.L. Low)
• J. McCarthy, On the Model Theory of Knowledge
• Neil GhaniFredrik Nordvall ForsbergEmail authorAlex Simpson, Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
• Finite Model Theory and its Applications
• D B MacQueen, G D Plotkin, R Sethi, An ideal model for recursive polymorphic types
• Nortström, Petersson, Smith, Programming in Martin-Löf's Type Theory
• Is there a known natural model of Peano Arithmetic where Goodstein's theorem fails?
• Geometric Model Theory
• Model Theory and Category Theory
• Theory of Objects Geometric Model Theory - hard reading, manifolds, algebraic geometry Model Theory and Category Theory - high level, but easy reading

Sets

• algebraic set theory (references)
• ncatlab, Material Set Theory
• Awodey, Butz, Simpson, Streicher, "Relating first-order set theories, toposes and categories of classes"
• Variation on Cubical sets
• Kripke–Platek set theory
• Algebraic Set Theory
• Set Theory for Computer Science
• Pocket Set Theory
• List of Set Theories
• Krivine, Realizability and forcing (Curry-Howard correspondence in set theory)
• The 8000th Busy Beaver number eludes ZF set theory

Michael A. Shulman

• Mike Shulman, Scones, Logical Relations, and Parametricity
• Comparing Material and Structural Set Theories
• From Set Theory to Type Theory
• SET THEORY FOR CATEGORY THEORY
• Rethinking Set Theory

Categories

• Joseph Goguen, Tossing the Algebraic Flowers Down the Great Divide
• Riehl, Categories in Context
• Riehl, ∞-categories for undergraduates
• François Métayer, Fixed points of functors
• Adamek, Fixed points of functors
• Lawvere's fixed point theorem
• Pierce’s Basic Category Theory for Computer Scientists – The Good Parts
• Dan Marsden, Category Theory Using String Diagrams
• Awesome #categorytheory, κζ-calculus vault
• Zeit Raffer: agda cats, idris cats
• Cat Theory for Scientists
• Free Applicative Functors
• me, Monad Genome
• wildcats
  • Knowledge base of 29 standard categories and several standard functors
  • User-definable categories, functors, natural transformations, universal properties, cones and other categorical constructions
  • State-of-the-art palette interface. Easily input all defined objects and operators (coming soon)
  • Automatic publish-quality generation of commutative and non-commutative diagrams
  • Visual functorial computations: apply a functor to a diagram and see the resulting diagram
  • Visual diagram evaluation: apply a diagram to an object and see the resulting diagram
  • Fully integrated documentation with 16 tutorial notebooks
  • Requires Mathematica® 8.x
• Oleksandr Manzyuk, Calculating monad transformers with category theory
• Reprints in Theory and Applications of Categories (list of works)
• Francis Borceux, Gilberte Van den Bossche, Categories of algebraic sheaves
• CMCS 2016, Fixed Points of Functors
• Joachim Kock, Notes on Polynomial Functors
• A Type-Theoretical Definition of Weak ω-Categories
• M.Stay, Category Theory in JavaScript
• C.Williams, M.Stay, Native Type Theory
• Chasing diagrams in cryptography
• Steven Lack, On the monadicity of finitary monads - that's about when a free monad may exist for a functor
• Finster, Reutter, A Type Theory for Strictly Unital ∞-Categories
• Introduction to Turing Categories
• Ian Stark, Free-Algebra Models for the π-Calculus
• Gershom Bazerman on "Homological Computations for Term Rewriting Systems"
• VARMO VENE, CATEGORICAL PROGRAMMING WITH INDUCTIVE AND COINDUCTIVE TYPES
• Marina Christina Lehner, All Concepts are Kan Extensions”
• Adámek, Fixed Points of Functors
• strong monads in cartesian-closed categories are applicative functors
• Giri monad
• Niles Johnson, Donald Yau, 2-Dimensional Categories
• Categorical programming language with effects (github)
• Visual Category Theory
• Applied Category Theory
• Yuri I. Manin, FORGOTTEN MOTIVES: THE VARIETIES OF SCIENTIFIC EXPERIENCE
• Riehl, Categories in Context
• Paranatural Category Theory
• Fixpoint in Computer Science (including Uustalo's paper on fixpoints and Yoneda Lemma for dinaturals

Type Theory

• Type Theory and Applications

HoTT

• HoTT, A Formalized Interpreter
• Course of HOTT
• Just Kidding: Understanding Identity Elimination in Homotopy Type Theory
• Yuri Manin, Matilde Marcolli, Homotopy Theoretic and Categorical Models of Neural Information Networks
• Introduction to HoTT

Optics

• Profunctor optics, a categorical update, by Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, and Mario Rom´an

General Math

• Patryshev, brief course in modern math
• Lehman, Leighton, Meyer, Mathematics for Computer Science (987 pages), or here, or here
• Math as hidden reality (video)
• В. А. Рохлин, Преподавание математики нематематикам
• Photos of Mathematicians
• New Foundations (wiki)
• Halmos on Applied Math
• Domain-Specific Languages of Mathematics: Presenting Mathematical Analysis Using Functional Programming
• большой список бесплатных книг
• Paul Taylor, Practical Foundations of Mathematics
• Linear Algebra Done Wrong Brett Wick, The Corona Problem
• VOEVODSKY’S UNACHIEVED PROJECT
• [Collatz conjecture calculator (27 is the worst)[https://www.dcode.fr/conjecture-syracuse]

Geometry

• Kissing problem in 4d solved (24)
• G.L.Litvinov, Tropical Mathematics, Idempotent Analysis, Classical Mechanics and Geometry
• School level geometry problems
• https://yigal-s.livejournal.com, 3d sections of a tesseract, video
• https://yigal-s.livejournal.com, 4d sections of a 5d hypercube
• Flat tori in three-dimensional space and convex integration
• Rotations of the three-sphere and symmetry of the Clifford Torus
• И. М. Гельфанд, З. Я. Шапиро, Представления группы вращений трёхмерного пространства и их применения

Automata

• Krohn-Rhodes

By Name

Baez

• Baez, Stay, Rosetta Stone
• Mysteries of Counting
• Deep Learning for a Categorist (slides)

Lawvere

• Complete Lawvere Works

Milewski

• Free Monoids, Functors, Categorically!
• Tambara Modules

Wadler

• Theorems for free!
• The Girard-Reynolds Isomorphism (second edition)
• Idioms are oblivious, arrows are meticulous, monads are promiscuous

Misc

• Книги в Московском центре непрерывного математического образования
• GRAMATICAS MATRICIALES DE GRAFOS
• Hinze, Wu, Gibbons, "Conjugate Hylomorphisms"
• Admissible numbering Rogers' equivalence theorem shows that all acceptable programming systems are equivalent to each other in the formal sense of numbering theory.
• Partial Commutative Monoids
• Jean-Yves Girard
• Mona: decidable arithmetic in practice
• Вавилов, Алгебры Клиффорда и Спинорные Группы, серия видео
• Exequiel Rivas, Mauro Jaskelioff, Notions of Computation as Monoids
• The Impact of seq on Free Theorems-Based Program Transformations
• Explicit Substitutions and Higher-Order Syntax
• Shut up and let me think! Or why you should work on the foundations of quantum mechanics as much as you please
• A THEORY OF TRANSFORMATION MONOIDS: COMBINATORICS AND REPRESENTATION THEORY
• Bukatin's essay on Penrose
• reflections on relativity
• Multi-scale Structural Complexity, code
• Reversible dynamics with closed time-like curves and freedom of choice
• Infinite Monkey Theorem
• Chaitin's Constant
• Normal Number
• Cantor Space
• Algorithmically Random Sequence
• Compositional Game Theory
• Gert Smolka, Confluence We study confluence of abstract relations and an abstract λβ-calculus parameterized with a function for β-reduction
• my other shit
• Dmitri Pavlov
• M.Bukatin, Generalized Distances and Generalized Equalities
• M.Bukatin, Partial Metrics and Quantale-valued Sets
• M.Bukatin, On Duality between Metric and Logical Viewpoints
• Quantale (nCatLab)
• Guillaume Lample, François Charton, "Deep Learning for Symbolic Mathematics"
• Buzzard, The Future of Math
• Counterexamples in Topology
• А.Ю. Пирковский, Спектральная теория и функциональные исчисления для линейных операторов
• Seven Trees in One
• My adventures with categories
• Kevin Buzzard, Richard Taylor, "A Blueprint for Fermat’s Last Theorem"

Formal Methods

• Formal Methods -- Course Notes
• Another formal methods course
• Readings in formal methods
• Intro to Formal Methods, Cornell
• [Software Engineering, Formal methods (Chalmers)
• Z book, alt
• Use of Formal Methods at Amazon Web Services

Extra stuff, temporary

https://wiki.nikiv.dev/ https://wiki.nikiv.dev/macOS/apps/karabiner/

MSPG Gavrilov

https://en.wikipedia.org/wiki/%C5%81ukasiewicz_logic https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Hilbert_system