CiteULike: pedagand's project-pre-phd [23 articles]

Types for Proofs and Programs (2002), pp. 727-727.

posted to data-type dependent-types project-pre-phd proof theorem-prover types by pedagand on 2009-07-12 23:05:37 as read

Practical Implementation of a Dependently Typed Functional Programming Language

(2005)

by Edwin Brady

posted to dependent-types language-epigram project-pre-phd by pedagand on 2009-07-03 22:35:08 as

Functional pearl: i am not a number--i am a free variable

In Haskell '04: Proceedings of the 2004 ACM SIGPLAN workshop on Haskell (2004), pp. 1-9.

by Conor Mcbride, James Mckinna

posted to lambda-calculus project-pre-phd by pedagand on 2009-07-03 22:06:38 as read

along with 2 people robertjohnsimmons spl

Proofs and types

(1989)

by Jean Y. Girard, Paul Taylor, Yves Lafont

posted to logic project-pre-phd types by pedagand on 2009-07-03 19:25:10 as read

along with 7 people and 1 group ddemange dimvar robertjohnsimmons robotact alec AndreasSchropp jonathlela ConcertRG

Categories of Containers

by Michael Abbott

posted to category-theory container-theory project-pre-phd by pedagand on 2009-07-03 19:20:07 as

A tutorial implementation of a dependently typed lambda calculus

Fundamenta Informaticae, Vol. XXI (2001), pp. 1001-1032.

by Andres Löh, Conor Mcbride, Wouter Swierstra

posted to dependent-types lambda-calculus project-pre-phd tutorial types by pedagand on 2009-07-03 19:11:14 as read

∂ for Data: Differentiating Data Structures

Fundam. Inf., Vol. 65, No. 1-2. (2004), pp. 1-28.

by Michael Abbott, Thorsten Altenkirch, Conor Mcbride, Neil Ghani

posted to container-theory project-pre-phd by pedagand on 2009-05-29 14:01:39 as read

The view from the left

J. Funct. Program., Vol. 14, No. 1. (January 2004), pp. 69-111.

by Conor Mcbride, James Mckinna

posted to dependent-types language-epigram project-pre-phd types by pedagand on 2009-05-26 10:53:58 as read

along with 7 people and 3 groups robertjohnsimmons spl jimburton byorgey dalev greenrd dmitri83 ConcertRG NU-PRL SRG_at_UCD

Type Theory and Functional Programming (International Computer Science Series)

by Simon Thompson

posted to dependent-types functional-programming project-pre-phd types by pedagand on 2009-04-20 14:32:41 as read

along with 2 people and 1 group mperalta rgrig SRG_at_UCD

Intuitionistic Type Theory

(1980)

by Per Martin-Löf

posted to dependent-types project-pre-phd types by pedagand on 2009-04-20 14:31:24 as read

along with 2 people greg_restall msakai

Programming in Martin-Löf's Type Theory: An Introduction

(19 July 1990)

by Bengt Nordstrom, Kent Petersson, Jan M. Smith

posted to dependent-types functional-programming project-pre-phd types by pedagand on 2009-04-20 14:29:31 as read

along with 2 people spl bringert

Generic Programming with Dependent Types

Datatype-Generic Programming (2007), pp. 209-257.

by Thorsten Altenkirch, Conor Mcbride, Peter Morris

posted to container-theory dependent-types generic-programming project-pre-phd types by pedagand on 2009-04-19 17:14:53 as read

Categories of Containers

Foundations of Software Science and Computation Structures (2003), pp. 23-38.

by Michael Abbott, Thorsten Altenkirch, Neil Ghani

posted to category-theory container-theory project-pre-phd by pedagand on 2009-04-19 17:05:24 as read

along with 1 person christiankissig

Constructing Universes for Generic Programming

(November 2007)

by Peter Morris

posted to container-theory dependent-types generic-programming project-pre-phd types by pedagand on 2009-04-19 16:47:40 as read

Observational equality, now!

In PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification (2007), pp. 57-68.

by Thorsten Altenkirch, Conor Mcbride, Wouter Swierstra

posted to dependent-types observational-equality project-pre-phd types by pedagand on 2009-04-19 16:40:41 as read

along with 3 people msakai noam_zeilberger Benja

Indexed Containers

by Thorsten Altenkirch, Peter Morris

posted to container-theory dependent-types generic-programming project-pre-phd types by pedagand on 2009-04-19 15:53:57 as read

Epigram reloaded: a standalone typechecker for ETT

In 6th Symposium on Trends in Functional Programming (September 2005)

by James Chapman, Thorsten Altenkirch, Conor Mcbride

posted to dependent-types language-epigram project-pre-phd type-checker types by pedagand on 2009-04-19 15:33:38 as read

A Universe of Strictly Positive Families

International Journal of Foundations of Computer Science, Vol. 20, No. 1. (2009), pp. 83-107.

by Peter Morris, Thorsten Altenkirch, Neil Ghani

posted to category-theory container-theory dependent-types language-epigram project-pre-phd types by pedagand on 2009-04-19 15:24:47 as read

The derivative of a regular type is its type of one-hole contexts

(2001)

by Conor Mcbride

posted to category-theory project-pre-phd zipper by pedagand on 2009-03-20 20:31:04 as read

along with 7 people and 2 groups robertjohnsimmons mattmight dherman eaubin zednenem josefs ryanc ConcertRG NU-PRL

Category Theory (Oxford Logic Guides)

(27 July 2006)

by Steve Awodey

posted to category-theory mathematics project-pre-phd by pedagand on 2009-02-12 02:10:52 as

along with 2 people NitinCR msakai

Basic Category Theory for Computer Scientists (Foundations of Computing)

(07 August 1991)

by Benjamin C. Pierce

posted to category-theory project-pre-phd types by pedagand on 2009-02-11 20:05:37 as

along with 12 people and 1 group fvogels olegus draganigajic ansobol jrw BarrosH proportional bonotake devnull Scis0000002 ds jimburton Lambda the Ultimate

Category Theory for Computing Science (Prentice-Hall International Series in Computer Science)

(25 August 1995)

by Michael Barr, Charles Wells

posted to category-theory project-pre-phd by pedagand on 2009-02-11 20:05:14 as

along with 3 people jimburton ds mmarcus

Epigram: Practical Programming with Dependent Types

Advanced Functional Programming (2005), pp. 130-170.

by Conor Mcbride

posted to dependent-types language-epigram lecture-cs-252r project-pre-phd types by pedagand on 2008-08-23 08:34:20 as read

along with 4 people and 1 group Benja jimburton draganigajic mcclurmc Lambda the Ultimate

	Elimination with a Motive [My Copy] Types for Proofs and Programs (2002), pp. 727-727. by Conor Mcbride posted to data-type dependent-types project-pre-phd proof theorem-prover types by pedagand on 2009-07-12 23:05:37 as
	Practical Implementation of a Dependently Typed Functional Programming Language [My Copy] (2005) by Edwin Brady posted to dependent-types language-epigram project-pre-phd by pedagand on 2009-07-03 22:35:08 as
	Functional pearl: i am not a number--i am a free variable [My Copy] In Haskell '04: Proceedings of the 2004 ACM SIGPLAN workshop on Haskell (2004), pp. 1-9. by Conor Mcbride, James Mckinna posted to lambda-calculus project-pre-phd by pedagand on 2009-07-03 22:06:38 as along with 2 people robertjohnsimmons spl
	Proofs and types [My Copy] (1989) by Jean Y. Girard, Paul Taylor, Yves Lafont posted to logic project-pre-phd types by pedagand on 2009-07-03 19:25:10 as along with 7 people and 1 group ddemange dimvar robertjohnsimmons robotact alec AndreasSchropp jonathlela ConcertRG
	Categories of Containers [My Copy] by Michael Abbott posted to category-theory container-theory project-pre-phd by pedagand on 2009-07-03 19:20:07 as
	A tutorial implementation of a dependently typed lambda calculus [My Copy] Fundamenta Informaticae, Vol. XXI (2001), pp. 1001-1032. by Andres Löh, Conor Mcbride, Wouter Swierstra posted to dependent-types lambda-calculus project-pre-phd tutorial types by pedagand on 2009-07-03 19:11:14 as
	∂ for Data: Differentiating Data Structures [My Copy] Fundam. Inf., Vol. 65, No. 1-2. (2004), pp. 1-28. by Michael Abbott, Thorsten Altenkirch, Conor Mcbride, Neil Ghani posted to container-theory project-pre-phd by pedagand on 2009-05-29 14:01:39 as
	The view from the left [My Copy] J. Funct. Program., Vol. 14, No. 1. (January 2004), pp. 69-111. by Conor Mcbride, James Mckinna posted to dependent-types language-epigram project-pre-phd types by pedagand on 2009-05-26 10:53:58 as along with 7 people and 3 groups robertjohnsimmons spl jimburton byorgey dalev greenrd dmitri83 ConcertRG NU-PRL SRG_at_UCD
	Type Theory and Functional Programming (International Computer Science Series) [My Copy] by Simon Thompson posted to dependent-types functional-programming project-pre-phd types by pedagand on 2009-04-20 14:32:41 as along with 2 people and 1 group mperalta rgrig SRG_at_UCD
	Intuitionistic Type Theory [My Copy] (1980) by Per Martin-Löf posted to dependent-types project-pre-phd types by pedagand on 2009-04-20 14:31:24 as along with 2 people greg_restall msakai
	Programming in Martin-Löf's Type Theory: An Introduction [My Copy] (19 July 1990) by Bengt Nordstrom, Kent Petersson, Jan M. Smith posted to dependent-types functional-programming project-pre-phd types by pedagand on 2009-04-20 14:29:31 as along with 2 people spl bringert
	Generic Programming with Dependent Types [My Copy] Datatype-Generic Programming (2007), pp. 209-257. by Thorsten Altenkirch, Conor Mcbride, Peter Morris posted to container-theory dependent-types generic-programming project-pre-phd types by pedagand on 2009-04-19 17:14:53 as
	Categories of Containers [My Copy] Foundations of Software Science and Computation Structures (2003), pp. 23-38. by Michael Abbott, Thorsten Altenkirch, Neil Ghani posted to category-theory container-theory project-pre-phd by pedagand on 2009-04-19 17:05:24 as along with 1 person christiankissig
	Constructing Universes for Generic Programming [My Copy] (November 2007) by Peter Morris posted to container-theory dependent-types generic-programming project-pre-phd types by pedagand on 2009-04-19 16:47:40 as
	Observational equality, now! [My Copy] In PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification (2007), pp. 57-68. by Thorsten Altenkirch, Conor Mcbride, Wouter Swierstra posted to dependent-types observational-equality project-pre-phd types by pedagand on 2009-04-19 16:40:41 as along with 3 people msakai noam_zeilberger Benja
	Indexed Containers [My Copy] by Thorsten Altenkirch, Peter Morris posted to container-theory dependent-types generic-programming project-pre-phd types by pedagand on 2009-04-19 15:53:57 as
	Epigram reloaded: a standalone typechecker for ETT [My Copy] In 6th Symposium on Trends in Functional Programming (September 2005) by James Chapman, Thorsten Altenkirch, Conor Mcbride posted to dependent-types language-epigram project-pre-phd type-checker types by pedagand on 2009-04-19 15:33:38 as
	A Universe of Strictly Positive Families [My Copy] International Journal of Foundations of Computer Science, Vol. 20, No. 1. (2009), pp. 83-107. by Peter Morris, Thorsten Altenkirch, Neil Ghani posted to category-theory container-theory dependent-types language-epigram project-pre-phd types by pedagand on 2009-04-19 15:24:47 as
	The derivative of a regular type is its type of one-hole contexts [My Copy] (2001) by Conor Mcbride posted to category-theory project-pre-phd zipper by pedagand on 2009-03-20 20:31:04 as along with 7 people and 2 groups robertjohnsimmons mattmight dherman eaubin zednenem josefs ryanc ConcertRG NU-PRL
	Category Theory (Oxford Logic Guides) [My Copy] (27 July 2006) by Steve Awodey posted to category-theory mathematics project-pre-phd by pedagand on 2009-02-12 02:10:52 as along with 2 people NitinCR msakai
	Basic Category Theory for Computer Scientists (Foundations of Computing) [My Copy] (07 August 1991) by Benjamin C. Pierce posted to category-theory project-pre-phd types by pedagand on 2009-02-11 20:05:37 as along with 12 people and 1 group fvogels olegus draganigajic ansobol jrw BarrosH proportional bonotake devnull Scis0000002 ds jimburton Lambda the Ultimate
	Category Theory for Computing Science (Prentice-Hall International Series in Computer Science) [My Copy] (25 August 1995) by Michael Barr, Charles Wells posted to category-theory project-pre-phd by pedagand on 2009-02-11 20:05:14 as along with 3 people jimburton ds mmarcus
	Epigram: Practical Programming with Dependent Types [My Copy] Advanced Functional Programming (2005), pp. 130-170. by Conor Mcbride posted to dependent-types language-epigram lecture-cs-252r project-pre-phd types by pedagand on 2008-08-23 08:34:20 as along with 4 people and 1 group Benja jimburton draganigajic mcclurmc Lambda the Ultimate

pedagand's project-pre-phd [23 articles] Export

pedagand's tags

functional-programming	88
language-haskell	85
operating-system	73
project-master-thesis	68
lecture-cs-252r	66
types	66
p2p	64
lecture-aos	37
dependent-types	36
formal-proof	35
category-theory	28
project-p2p-theory	28
compiler	26
lecture-sdr	26
monads	25
programming-language	25
gossip	24
project-pre-phd	23
distributed	22
lecture-cse-551	22
lecture-acnds	21
file-system	20
software-verification	20
architecture	17
lecture-vts	17
coq	16
system-programming	16
virtualization	16
optimization	15
parallel	15
concurrency	14
distributed-systems	14
lecture-pas	14
multicast	12
container-theory	11
lecture-pap	11
chemical-abstract-machine	10
domain-specific-language	10
generic-programming	10
lecture-asr	10
networking	10
semantics	10
sigcomm-recommended-reading	10
stm	10
testing	10
dht	9
functional-reactive	9
interpreter	9
specification	9
abstract-interpretation	8
caml	8
data-flow	8
device-driver	8
ml	8
network	8
project-schame	8
tool-tla	8
homework-sdr-1	7
incentives	7
language-ivy	7
lecture-pev	7
multiset	7
parallel-computing	7
project-stream-theory	7
timed-automata	7
type-classes	7
algebra-of-programming	6
bulk-data-transport	6
certification	6
coinduction	6
coq-programming	6
free-rider	6
garbage-collection	6
grid-computing	6
inter-process-communication	6
lambda-calculus	6
language-agda	6
language-c	6
language-epigram	6
language-java	6
lecture-dac	6
lock-free	6
model-checking	6
proof	6
reactive-language	6
real-time	6
worms	6
arrows	5
capability	5
containment	5
cps	5
data-structure	5
exceptions	5
gamma-model	5
homework-pas-1	5
hybrid-types	5
isabelle	5
mathematics	5
mechanization	5
project-phd-thesis	5
proof-simulation	5
threads	5
typed-assembly-language	5
binary-decision-diagram	4
bittorrent	4
clock-vector	4
consensus	4
crypto	4
distributed-computing	4
fair-sharing	4
functional-circuit	4
homework-vts-1	4
io-automata	4
join-calculus	4
lambda-machine	4
language	4
language-deputy	4
language-mace	4
lava	4
lazy-language	4
meta-compilation	4
pastry	4
performance-debugging	4
physic	4
polymorphism	4
project-opis	4
remote-procedure-calls	4
scheduler	4
sybil-attack	4
theorem-prover	4
thread-implementation	4
time	4
type-checker	4
universe	4
asynchronous-exceptions	3
binary-translation	3
byzantine-fault	3
cache	3
continuations	3
dataflow-analysis	3
dynamic-code-loading	3
embedded	3
event-driven	3
formalization	3
hardware-design	3
ia-64	3
lisp	3
lucid-synchrone	3
multi-threading	3
nooks	3
parallel-io	3
pointer-analysis	3
protocol	3
pure	3
security	3
sequent-calculus	3
shared-memory	3
state-machines	3
streaming	3
synchronous-language	3
tactic	3
translation-validation	3
type-refinement	3
types-gadt	3
zipper	3
aspect-oriented-programming	2
asynchronous-system	2
bidirectionalization	2
broadcasting	2
calculus-of-construction	2
can	2
causal-order	2
churn	2
combinator	2
comonad	2
computing	2
concurrent-ml	2
congestion-control	2
control-flow	2
cryptanalysis	2
ddos	2
defunctionalization	2
effects	2
event	2
failure-detector	2
fpga	2
free-theorems	2
graph-reduction	2
graph-theory	2
higher-order	2
hol	2
homework-pev-1	2
information-flow	2
interface-definition-language	2
jahob	2
java-bytecode	2
kleisli-structures	2
label-based-security	2
language-bitc	2
language-clean	2
language-scheme	2
language-vault	2
lattice	2
linear-types	2
logic-programming	2
map-reduce	2
memory-management	2
mesh	2
micro-kernel	2
monadic-region	2
multi-core	2
mutual-exclusion	2
network-location-service	2
object-storage	2
open-problem	2
os-k42	2
os-sel4	2
os-singularity	2
ott	2
partial-order	2
precomputation	2
probability	2
project-scale-max	2
pushdown-timed-automata	2
quicksilver	2
rely-guarantee	2
safety-violation	2
scheme	2
simulation	2
social-network	2
software-based-fault-isolation	2
stream-processor	2
system-f	2
test-selection	2
thermodynamics	2
time-analysis	2
time-memory	2
tool-cal	2
tool-kddm	2
tool-valgrind	2
topology	2
trade-off	2
transaction	2
tree	2
trust	2
type	2
type-inference	2
vliw	2
writing	2
xen	2
xml	2
active-network	1
adaptive	1
agreement-problem	1
algebra	1
applicative	1
asic	1
attribute-grammar	1
automated-theorem-prover	1
automatic-mutual-exclusion	1
axiomatic-analysis	1
backup-system	1
bayeux	1
bidirectional	1
black-box	1
blame-calculus	1
branch-prediction	1
bullet	1
calculus	1
clock-matrix	1
cluster	1
code-generation	1
code-propagation	1
coherency	1
component-programming	1
comprehension	1
computational-power	1
computer-history	1
computer-mathematics	1
constraint-based-analysis	1
contracts	1
coproducts	1
credible-compilation	1
cyclon	1
datalog	1
data-type	1
debugging	1
declarative	1
delimited-continuations	1
denali	1
derivative	1
digital-fountain	1
dmt	1
documentation	1
dps	1
driver-protocol-state-machine	1
effect	1
equational-reasoning	1
erasure-correcting-codes	1
experimentation	1
expression-problem	1
expressive-power	1
finance	1
finite-state-machine	1
floating-point-arithmetic	1
flp	1
fluid-model	1
flux-oskit	1
fold	1
functional-dependencies	1
generational-gc	1
gradual-types	1
hash	1
herlihy-hierarchy	1
hive	1
hoare-type-theory	1
homework-pap-1	1
hot-code-swapping	1
idl-hdirect	1
idl-idl4	1
imperative-programming	1
impossibility-result	1
impure	1
internet	1
io-characterization	1
iolts	1
io-scheduling	1
isa	1
itanium	1
kahn-network	1
kernel	1
language-atomcaml	1
language-bpl	1
language-clight	1
language-cpp	1
language-fp	1
language-gofer	1
language-miranda	1
language-oleg	1
language-sml	1
language-spec	1
language-tame	1
language-vbasic	1
lazy-receiver-processing	1
leader-election	1
lectiure-asr	1
lecture-os-prelim	1
library-communication	1
linear-algebra	1
linear-restraints	1
literate-programming	1
live-objects	1
llvm	1
logic	1
lustre	1
macro	1
manual-memory-management	1
memory-coherence	1
memory-model	1
memory-protection	1
meridian	1
metal	1
meta-mathematics	1
meta-programming	1
method-mixins	1
mips	1
modulo-scheduling	1
mondriaan	1
mpi-io	1
multi-language	1
natural-semantics	1
nfs	1
noninterference	1
normalization	1
observational-equality	1
orc	1
os-asbestos	1
os-barrelfish	1
os-fluke	1
os-histar	1
os-mungi	1
os-nexus	1
os-scout	1
ossification	1
os-spring	1
os-unix	1
partial-evaluation	1
pipeline	1
polymorphic	1
precise-interrupts	1
printf	1
process-calculus	1
project-proofxml	1
project-timed-semantics	1
proof-carrying-code	1
prover-lego	1
pushdown-automata	1
qualified-types	1
quotient-types	1
r1000	1
raid	1
randomization	1
randomized-algorithm	1
reconfigurable-computing	1
recovery	1
refactoring	1
reference-pointer	1
reflection-proof	1
region-memory	1
registers-renaming	1
relational-language	1
review	1
router-software	1
scribe	1
semantic-overlay	1
semantics-operational	1
sensor-network	1
separation-logic	1
session-types	1
set-theory	1
small-world	1
sml	1
smt	1
soft-types	1
stack-ripping	1
stateful-computation	1
stateless-kernel	1
statistics	1
stealth	1
structured-gamma	1
surjective-pairing	1
synchronisation	1
synchronous-system	1
system-on-chip	1
taint	1
tangible-values	1
tapestry	1
tcp-ip	1
tool-astec	1
tool-bddbddb	1
tool-ccomment	1
tool-cil	1
tool-concierge	1
tool-hdirect	1
tool-hoopl	1
tool-kdfs	1
total-functional-programming	1
tutorial	1
type-soundness	1
types-phantom	1
uniform-reliable-broadcast	1
uniform-type-theory	1
units-of-measure	1
unparsing	1
user-remote-procedure-calls	1
virtual-money	1
vivaldi	1
vod	1
wait-free	1
warm-up	1
wired	1
worst-case-execution-time	1
xcp	1
xorp	1
zfc	1