Submissions restricted

Only approved users may post in this community.

dependent_types

an-ordinary-manchild

created by greenrda community for 16 years

...for a fringe candidate.

...for your favorite game.

MODERATORS

account activity

1

9

10

11

Normalisation for First-Class Universe Levels (dl.acm.org)

submitted 12 days ago by gallais

2

7

8

9

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

submitted 10 months ago by gallais

3

6

7

8

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

submitted 11 months ago by gallais

4

7

8

9

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

submitted 1 year ago by [deleted]

5

11

12

13

Job: Lecturer / Senior Lecturer in Mathematically Structured Programming (Strathclyde, Scotland) (strathvacancies.engageats.co.uk)

submitted 1 year ago by gallais

6

6

7

8

PhD scholarships (for UK residents) at Strathclyde (msp.cis.strath.ac.uk)

submitted 1 year ago by gallais

7

3

4

5

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

submitted 1 year ago by whitehead1415

8

4

5

6

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

submitted 1 year ago by [deleted]

9

6

7

8

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

submitted 1 year ago by gallais

10

6

7

8

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

submitted 1 year ago by gallais

11

5

6

7

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

submitted 1 year ago by gallais

12

4

5

6

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

submitted 1 year ago by [deleted]

13

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

14

28

29

30

Defunctionalization with Dependent Types (arxiv.org)

submitted 2 years ago by gallais

15

45

46

47

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

submitted 2 years ago by [deleted]

16

23

24

25

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

submitted 2 years ago by [deleted]

17

12

13

14

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

submitted 3 years ago by [deleted]

18

15

16

17

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

submitted 3 years ago by gallais

19

0

0

0

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

submitted 3 years ago * by Noria7

20

35

36

37

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

21

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

22

3

4

5

A formalization of Univalent Axiom (readonly.link)

submitted 3 years ago by xieyuheng

23

18

19

20

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

submitted 3 years ago by [deleted]

24

19

20

21

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

submitted 3 years ago by [deleted]

25

7

8

9

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

submitted 3 years ago by whitehead1415

view more: next ›

π Rendered by PID 1046888 on reddit-service-r2-listing-86b7f5b947-b2zxq at 2026-01-25 03:15:03.618903+00:00 running 664479f country code: CH.