Sciweavers

PLPV
2009
ACM
14 years 8 months ago
Type invariants for Haskell
Haskell’s multi-parameter type classes, together with functional dependencies, allow the specification of complex type-level opera
Tom Schrijvers, Louis-Julien Guillemette, Stefan M...
PLPV
2009
ACM
14 years 8 months ago
Verified programming in Guru
Aaron Stump, Morgan Deters, Adam Petcher, Todd Sch...
PLPV
2009
ACM
14 years 8 months ago
Embedding a logical theory of constructions in Agda
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...
PLPV
2009
ACM
14 years 8 months ago
Positively dependent types
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