NEW BOT Телеграм, страница

Pure & constructive mathematics in theory and use

Category Theory
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.211.4754&rep=rep1&type=pdf

728 viewsUnivalence (apparently does haskell tech support), 19:18

Pure & constructive mathematics in theory and use

Normal Derivability and First-Order Arithmetic
https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093883058

projecteuclid.org

Tosi : Normal derivability and first-order arithmetic.

Project Euclid - mathematics and statistics online

457 viewsUnivalence (apparently does haskell tech support), 13:11

Pure & constructive mathematics in theory and use

Approximating Inductive Types in Coq
https://gmalecha.github.io/reflections/2016/approximating-inductive-types

gmalecha.github.io

Approximating Inductive Types in Coq | Gregory Malecha

I do research on programming languages, program verification, compilers, and program analysis.

468 viewsptrcmd, edited 07:21

Pure & constructive mathematics in theory and use

How to Write Seemingly Unhygienic and Referentially Opaque Macros with Syntax-rules
http://okmij.org/ftp/Scheme/Dirty-Macros.pdf
A bit more programming-related, but still close enough to matter :)
[Thanks to Freddie]

556 viewsUnivalence (apparently does theorem proving tech support), 19:36

Pure & constructive mathematics in theory and use

Fast and Loose Reasoning is Morally Correct
https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf

505 viewsUnivalence (apparently does theorem proving tech support), 18:00

Pure & constructive mathematics in theory and use

Understanding and Using Spector’s Bar Recursive Interpretation of Classical Analysis
https://www.eecs.qmul.ac.uk/~pbo/papers/paper011.pdf

549 viewsptrcmd, 18:01

Pure & constructive mathematics in theory and use

Elements of Finite Model Theory
https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf

501 viewsUnivalence (apparently does theorem proving tech support), 17:52

Pure & constructive mathematics in theory and use

Model theory Notes
https://math.berkeley.edu/~scanlon/225af13lectures/ModelTheoryNotes.pdf

559 viewsUnivalence (apparently does theorem proving tech support), 20:39

Pure & constructive mathematics in theory and use

Small update on Multicore OCaml
https://discuss.ocaml.org/t/where-is-multicore-development-happening/4997/8?u=yawaramin

OCaml

Where is Multicore development happening?

Hopefully this is a pretty simple question, with the first hunk of multicore support being submitted upstream in mid-2019, where is OCaml multicore development happening? Is it still at the ocamllabs repo? The last commit there is 2 months ago and looks like…

522 viewsGNU/Brett G., 20:49

Pure & constructive mathematics in theory and use

MaPLe: a parallel compiler extension to MLton
https://github.com/MPLLang/mpl

GitHub

GitHub - MPLLang/mpl: The MaPLe compiler: efficient and scalable parallel functional programming

The MaPLe compiler: efficient and scalable parallel functional programming - MPLLang/mpl

416 viewsGNU/Brett G. (Away), 20:05

Pure & constructive mathematics in theory and use

Lean versus Coq: The cultural chasm
https://artagnon.com/articles/leancoq

410 viewsGNU/Brett G. (Away), 20:53

Pure & constructive mathematics in theory and use

From setoid hell to homotopy heaven? The role of extensionality in Type Theory
http://www.cs.nott.ac.uk/~psztxa/talks/types-17-hell.pdf
[Thanks to Elias]

378 viewsUnivalence (apparently does theorem proving tech support), 21:16

Pure & constructive mathematics in theory and use

The Arend Theorem Prover - A Tutorial
https://arend-lang.github.io/documentation/tutorial

389 viewsTesla Zhang, edited 21:43

Pure & constructive mathematics in theory and use

Various new theorems in constructive univalent mathematics written in Agda
https://github.com/martinescardo/TypeTopology

GitHub

GitHub - martinescardo/TypeTopology: Logical manifestations of topological concepts, and other things, via the univalent point…

Logical manifestations of topological concepts, and other things, via the univalent point of view. - martinescardo/TypeTopology

379 viewsUnivalence (apparently does theorem proving tech support), 20:06

Pure & constructive mathematics in theory and use

Felis: Common Category Theoretic Abstractions for Standard ML
https://github.com/Saityi/felis

GitHub

Saityi/felis

(⚠️ Work in Progress ⚠️) Category theoretic abstractions and implementations - Saityi/felis

572 viewsGNU/Brett G., 20:10

Pure & constructive mathematics in theory and use

Forwarded from Arend notes

https://github.com/arend-lang/tutorial-code

GitHub

arend-lang/tutorial-code

Source code & exercises in Arend's documentation. Contribute to arend-lang/tutorial-code development by creating an account on GitHub.

59 viewsTesla Zhang, 20:10

Pure & constructive mathematics in theory and use

Abstract Algebra - Theory and Applications
https://www.math.colostate.edu/~pries/467/Judson12.pdf

427 viewsUnivalence (apparently does theorem proving tech support), 12:57

Pure & constructive mathematics in theory and use

Vale
https://github.com/project-everest/vale

GitHub

GitHub - project-everest/vale: Verified Assembly Language for Everest

Verified Assembly Language for Everest. Contribute to project-everest/vale development by creating an account on GitHub.

434 viewsUnivalence | install guix, 21:29

Pure & constructive mathematics in theory and use

13th International Conference on Graph Transformation
ICGT 2020
http://icgt2020.di.unipi.it
co-located with STAF 2020, June 22-26 Bergen, Norway

ICGT 2020

Home

492 viewsGNU/Brett G., 21:34

Pure & constructive mathematics in theory and use

Fifth International Conference on
Formal Structures for Computation and Deduction (FSCD 2020)
June 29 – July 5, 2020, Paris, France
http://fscd2020.org/

702 viewsGNU/Brett G., 21:37

Pure & constructive mathematics in theory and use

Learn Standard ML & Ponyo
https://ponyo.org/guides

ponyo.org

Ponyo - Library and Toolkit for Standard ML

Library and Toolkit for Standard ML.

543 viewsGNU/Brett G., 02:53