Sciweavers

35

PLPV
2009
ACM

87views Programming Languages» more PLPV 2009»

Pragmatic equivalence and safety checking in Cryptol

14 years 6 months ago

Pragmatic equivalence and safety checking in Cryptol

Download www.galois.com

Levent Erkök, John Matthews

claim paper

Read More »

30

PLPV
2009
ACM

101views Programming Languages» more PLPV 2009»

Type invariants for Haskell

14 years 8 months ago

Type invariants for Haskell

Download www.cs.kuleuven.be

Haskell’s multi-parameter type classes, together with functional dependencies, allow the speciﬁcation of complex type-level opera

Tom Schrijvers, Louis-Julien Guillemette, Stefan M...

claim paper

Read More »

30

PLPV
2009
ACM

80views Programming Languages» more PLPV 2009»

Verified programming in Guru

14 years 8 months ago

Verified programming in Guru

Download guru-lang.googlecode.com

Aaron Stump, Morgan Deters, Adam Petcher, Todd Sch...

claim paper

Read More »

47

PLPV
2009
ACM

174views Programming Languages» more PLPV 2009»

Embedding a logical theory of constructions in Agda

14 years 8 months ago

Embedding a logical theory of constructions in Agda

Download www.cs.chalmers.se

We propose a new way to reason about general recursive functional programs in the dependently typed programming language Agda, which is based on Martin-L¨of’s intuitionistic ty...

Ana Bove, Peter Dybjer, Andrés Sicard-Ram&i...

claim paper

Read More »

40

PLPV
2009
ACM

142views Programming Languages» more PLPV 2009»

Positively dependent types

14 years 8 months ago

Positively dependent types

Download www.cs.cmu.edu

This paper is part of a line of work on using the logical techniques of polarity and focusing to design a dependent programming language, with particular emphasis on programming w...

Daniel R. Licata, Robert Harper

claim paper

Read More »