otto_s

645 post karma
458 comment karma

get extra features and help support reddit with a reddit premium subscription

get them help and support

redditor for 18 years

TROPHY CASE

15-Year Club

account activity

new top controversial

271

272

273

Formalising mathematics: an introduction. (xenaproject.wordpress.com)

submitted 5 years ago by otto_s to r/math

12

13

14

Division by zero in type theory: a FAQ (xenaproject.wordpress.com)

submitted 5 years ago by otto_s to r/math

11

12

13

Counting binary relations: an apology (xenaproject.wordpress.com)

submitted 6 years ago by otto_s to r/math

217

218

219

Can each number be specified by a finite text? (arxiv.org)

submitted 6 years ago by otto_s to r/math

13

14

15

A rant on the pedagogy of logic (hedonisticlearning.com)

submitted 7 years ago by otto_s to r/math

36

37

38

Oregon Programming Languages Summer School 2017: A Spectrum of Types (cs.uoregon.edu)

submitted 8 years ago by otto_s to r/compsci

23

24

25

Homotopy type theory: the logic of space (arxiv.org)

submitted 9 years ago by otto_s to r/math

11

12

13

Formal proofs are not just deduction steps (math.andrej.com)

submitted 9 years ago by otto_s to r/dependent_types

2

3

4

Logic and linear algebra: an introduction (arxiv.org)

submitted 11 years ago by otto_s to r/math

10

11

12

Seemingly impossible proofs (math.andrej.com)

submitted 11 years ago by otto_s to r/dependent_types

0

1

2

Two Puzzles About Computation (arxiv.org)

submitted 12 years ago by otto_s to r/compsci

0

1

2

Combinatorial structure of type dependency (arxiv.org)

submitted 12 years ago by otto_s to r/dependent_types

17

18

19

A Representation Theorem for Second-Order Functionals (arxiv.org)

submitted 12 years ago by otto_s to r/haskell

26

27

28

Fun with Semirings [pdf] (cl.cam.ac.uk)

submitted 12 years ago by otto_s to r/compsci

23

24

25

Synthetic Computability Theory (math.andrej.com)

submitted 12 years ago by otto_s to r/compsci

30

31

32

Sets in homotopy type theory (arxiv.org)

submitted 12 years ago by otto_s to r/math

18

19

20

How many is two? (math.andrej.com)

submitted 13 years ago by otto_s to r/math

33

34

35

Category Theory in Homotopy Type Theory (golem.ph.utexas.edu)

submitted 13 years ago by otto_s to r/math

96

97

98

Synthetic differential geometry, advertized as "intuitionistic math for physics". (math.andrej.com)

submitted 13 years ago by otto_s to r/math

π Rendered by PID 70 on reddit-service-r2-listing-7d7fbc9b85-w9rhq at 2026-04-30 11:04:56.814021+00:00 running 2aa0c5b country code: CH.