types

+ frontpage - frontpage1,271 readers

a community for 3 years

to anything interesting: news article, blog entry, video, picture...

message the moderators

MODERATORS

japple

1

10

11

12

Oregon Programming Languages Summer School - Logic, Languages, Compilation, and Verification (lectures, including video) (cs.uoregon.edu)

submitted 4 days ago by drdo

2

6

7

8

What is this thing you call a "type"? Part Two - Eric Lippert (blogs.msdn.com)

submitted 5 days ago by japple

3

1

2

3

brand new Ωmega 1.5.1 and a teaser... (code.google.com)

submitted 5 days ago by heisenbug

4

2

3

4

Why do so many theories use first-class constructors instead of sum (disjunction) types? (self.types)

submitted 10 days ago by whatsheon

5

13

14

15

Why Homotopy Type Theory? (self.types)

submitted 11 days ago by whatsheon

6

2

3

4

Simplifying Recursive Types in Whiley (whiley.org)

submitted 13 days ago by redjamjar

7

11

12

13

Systems Programming with Dependent Types (edwinb.wordpress.com)

submitted 16 days ago by japple

8

5

6

7

new version of lib for binding names (GADT support!) (byorgey.wordpress.com)

submitted 18 days ago by heisenbug

9

8

9

10

Coquet: a Coq library for verifying hardware (arxiv.org)

submitted 20 days ago by japple

10

2

3

4

AskTypes: Introductory material for type theory? (self.types)

submitted 1 month ago by orbat

11

17

18

19

How I learned to stop worrying and love de Bruijn indices (disciple-devel.blogspot.com)

submitted 1 month ago by japple

12

8

9

10

Fully-Funded PhD Studentship in Functional Programming (cs.nott.ac.uk)

submitted 2 months ago by grahamhutton

13

10

11

12

Why Verify Software? (blog.regehr.org)

submitted 2 months ago by japple

14

4

5

6

Constructive gem: an injection from Baire space to natural numbers (math.andrej.com)

submitted 2 months ago by japple

15

7

8

9

Type preservation as a confluence problem (cs.uiowa.edu)

submitted 3 months ago by inaneInTheMembrane

16

4

5

6

Type Inference for Bimorphic Recursion (arxiv.org)

submitted 3 months ago by japple

17

1

2

3

I have a few questions about the implications of the rule of cumulativity being used in the Calculus of Constructions (self.types)

submitted 3 months ago by whatsheon

18

10

11

12

Transformations as strict groupoids (existentialtype.wordpress.com)

submitted 3 months ago by japple

19

16

17

18

Higher-Dimensional Type Theory (existentialtype.wordpress.com)

submitted 3 months ago by japple

20

15

16

17

Bedrock, a Coq library for verified low-level programming (adam.chlipala.net)

submitted 3 months ago by japple

21

17

18

19

Computer certified efficient exact reals in Coq (arxiv.org)

submitted 3 months ago by japple

22

2

3

4

Post on /r/compsci: Interesting secrets of formal methods in the real world (reddit.com)

submitted 4 months ago by japple

23

2

3

4

A Step-indexed Semantic Model of Types for the Call-by-Name Lambda Calculus (front.math.ucdavis.edu)

submitted 4 months ago by japple

24

4

5

6

Is the Ceylon type system sound? (in.relation.to)

submitted 4 months ago by gst

25

13

14

15

Embedded in Academia : An Executable Semantics For C Is Useful (blog.regehr.org)

submitted 4 months ago by japple

view more: next