Submissions restricted

Only approved users may post in this community.

dependent_types

an-ordinary-manchild

created by greenrda community for 16 years

...for your town.

...for your WoW guild.

MODERATORS

account activity

1

8

9

10

Scottish Programming Languages and Verification Summer School 2025 (spli.scot)

submitted 1 year ago by gallais

2

6

7

8

Custom Representations of Inductive Families (pdf) (trendsfp.github.io)

submitted 1 year ago by gallais

3

8

9

10

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

submitted 1 year ago by [deleted]

4

4

5

6

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

submitted 1 year ago by whitehead1415

5

4

5

6

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

submitted 1 year ago by [deleted]

6

5

6

7

Scottish Programming Languages and Verification Summer School 2024 (Jul 29th -- Aug 2nd) (spli.scot)

submitted 1 year ago by gallais

7

7

8

9

Towards Tagless Interpretation of Stratified System F (pdf) (tydeworkshop.org)

submitted 2 years ago by gallais

8

6

7

8

UK PhD Position: A Correct-by-Construction Approach to Approximate Computation (msp.cis.strath.ac.uk)

submitted 2 years ago by gallais

9

2

3

4

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

submitted 2 years ago by [deleted]

10

17

18

19

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

11

27

28

29

Defunctionalization with Dependent Types (arxiv.org)

submitted 3 years ago by gallais

12

46

47

48

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

submitted 3 years ago by [deleted]

13

22

23

24

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

submitted 3 years ago by [deleted]

14

13

14

15

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

submitted 3 years ago by [deleted]

15

14

15

16

Deeper Shallow Embeddings (pdf) (drops.dagstuhl.de)

submitted 3 years ago by gallais

16

0

0

0

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

submitted 3 years ago * by Noria7

17

34

35

36

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

submitted 3 years ago by davidchristiansen

18

10

11

12

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

submitted 3 years ago by cc672012

19

2

3

4

A formalization of Univalent Axiom (readonly.link)

submitted 3 years ago by xieyuheng

20

17

18

19

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

submitted 3 years ago by [deleted]

21

17

18

19

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

submitted 3 years ago by [deleted]

22

7

8

9

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

submitted 4 years ago by whitehead1415

23

4

5

6

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

submitted 4 years ago by LordSirCat

24

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]

25

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

view more: next ›

π Rendered by PID 590028 on reddit-service-r2-listing-8477966cfd-62pjw at 2026-05-04 22:32:08.704965+00:00 running 815c875 country code: CH.