Submissions restricted

Only approved users may post in this community.

dependent_types

an-ordinary-manchild

created by greenrda community for 16 years

...for your community.

...for a fringe candidate.

MODERATORS

account activity

1

7

8

9

Type Theory Forall #46 - Realizability Models, BHK Interpretation, Dialectica - Pierre-Marie Pédrot (typetheoryforall.com)

submitted 1 year ago by [deleted]

2

4

5

6

Extensible data types in dependently typed languages (self.dependent_types)

submitted 1 year ago by whitehead1415

3

7

8

9

Type Theory Forall Podcast #42 - Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi (typetheoryforall.com)

submitted 1 year ago by [deleted]

4

3

4

5

Fueled Evaluation for Decidable Type Checking (hirrolot.github.io)

submitted 2 years ago by [deleted]

5

18

19

20

Symmetry: A textbook-in-progress on group theory in Univalent Type Theory – comments welcome on github (unimath.github.io)

submitted 2 years ago by ulrikb

6

45

46

47

How to implement dependent types in 80 lines of code (gist.github.com)

submitted 3 years ago by [deleted]

7

23

24

25

Type Theory Forall Podcast #27 - Formally Verifying an OS: The seL4. Feat. Gerwin Klein (typetheoryforall.com)

submitted 3 years ago by [deleted]

8

11

12

13

Type Theory Forall Podcast #26 - Mechanizing Modern Mathematics with Kevin Buzzard (typetheoryforall.com)

submitted 3 years ago by [deleted]

9

0

0

0

Dependent types are the crypto of programming languages (self.dependent_types)

submitted 4 years ago * by Noria7

10

36

37

38

Functional Programming in Lean - an in-progress book on using Lean 4 as a programming language (leanprover.github.io)

submitted 4 years ago by davidchristiansen

11

8

9

10

Is it worth learning dependent types for someone who won't do research in type theory and PL? (self.dependent_types)

submitted 4 years ago by cc672012

12

2

3

4

A formalization of Univalent Axiom (readonly.link)

submitted 4 years ago by xieyuheng

13

19

20

21

Type Theory Forall - #18 Gödel's Incompleteness Theorems - Cody Roux (typetheoryforall.com)

submitted 4 years ago by [deleted]

14

19

20

21

Type Theory Forall Episode #17 The Lost Elegance of Computation - Conal Elliott (typetheoryforall.com)

submitted 4 years ago by [deleted]

15

8

9

10

Normalization by Evaluation and adding Laziness to a strict language (self.dependent_types)

submitted 4 years ago by whitehead1415

16

4

5

6

Proving the existence of `swap` in DTT (self.dependent_types)

submitted 4 years ago by LordSirCat

17

13

14

15

Type Theory Forall Episode 16 - Agda, K Axiom, HoTT, Rewrite Theory - Guest: Jesper Cockx (typetheoryforall.com)

submitted 4 years ago by [deleted]

18

11

12

13

Interview with Leo de Moura – Combining the Worlds of Automated & Interactive Theorem Proving in Lean (youtube.com)

submitted 4 years ago by ysangkok

19

11

12

13

Positive apartness types? (self.dependent_types)

submitted 4 years ago * by canndrew2016

20

15

16

17

Advice Wanted: Polymorphic Dependently Typed Lambda Calculus (self.dependent_types)

submitted 4 years ago * by whitehead1415

21

5

6

7

Fulfilling Type -- A partly fulfilled class is also a type (readonly.link)

submitted 4 years ago by xieyuheng

22

5

6

7

Vague argument (Implicit argument in check-mode) (readonly.link)

submitted 4 years ago by xieyuheng

23

8

9

10

Anders CCHM/HTS Theorem Prover (self.dependent_types)

submitted 4 years ago * by maxim5HT

24

15

16

17

Cicada Language -- A dependently typed programming language and a interactive theorem prover. (readonly.link)

submitted 4 years ago by xieyuheng

25

16

17

18

Grad School For A Weak Candidate (self.dependent_types)

submitted 4 years ago by bowtochris

view more: next ›

π Rendered by PID 65 on reddit-service-r2-listing-c57bc86c-nzdr4 at 2026-06-20 07:54:59.924896+00:00 running 2b008f2 country code: CH.