mvermaat's coq [16 articles] Export

Recent papers added to mvermaat's library classified by the tag coq. You can also see everyone's coq.

	Certified Programming with Dependent Types [My Copy] (2009) by Adam Chlipala posted to verification types theorem-proving logic literature-study functional-programming dependent-types coq compilers binding bachelor-project by mvermaat on 2009-11-16 18:02:13 as
	An application of co-inductive types in Coq: Verification of the alternating bit protocol [My Copy] Types for Proofs and Programs (1996), pp. 135-152. by Eduardo Giménez posted to verification theorem-proving recursion master-project logic functional-programming coq coinduction by mvermaat on 2009-11-05 14:02:51 as
	A Tutorial on Recursive Types in Coq [My Copy] INRIA ROCQUENCOURT (1998) by Eduardo Giménez posted to types recursion master-project logic functional-programming coq coinduction by mvermaat on 2009-11-05 13:34:58 as
	Well-foundedness of the recursive path ordering in Coq [My Copy] In Dutch Proof Tools Day 2004 (July 2004) by Nicole de Kleijn, Adam Koprowski, Femke van Raamsdonk posted to theorem-proving termination rpo rewriting master-project coq by mvermaat on 2009-09-30 00:30:32 as
	Well-foundedness of RPO in Coq [My Copy] (August 2003) by Nicole de Kleijn posted to theorem-proving termination rpo rewriting master-project coq by mvermaat on 2009-09-30 00:24:50 as
	A Tutorial on [Co-]Inductive Types in Coq [My Copy] (2007) by Eduardo Giménez, Pierre Castéran posted to types master-project functional-programming coq coinduction by mvermaat on 2009-09-30 00:01:17 as
	Engineering formal metatheory [My Copy] In POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (2008), pp. 3-15. by Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich posted to binding coq lambda-calculus literature-study poplmark by mvermaat on 2009-02-13 11:08:52 as along with 3 people and 1 group fvogels bdauvergne marcinzalewski ConcertRG
	Adbmal [My Copy] In Proceedings CADE-19, Vol. 2741 (2003), pp. 136-150. by Dimitri Hendriks, Vincent van Oostrom edited by F. Baader posted to binding coq lambda-calculus syntax by mvermaat on 2009-02-06 14:30:40 as
	Higher Order Abstract Syntax in Type Theory [My Copy] In Logic Colloquium 2006 (2006) by Venanzio Capretta, Amy Felty posted to binding coq poplmark types by mvermaat on 2009-01-14 13:08:03 as
	POPLmark 1a with Named Bound Variables [My Copy] (2005) by Aaron Stump posted to coq literature-study poplmark theorem-proving types by mvermaat on 2008-04-17 11:41:44 as
	Theorem proving support in programming language semantics [My Copy] (6 Jul 2007) by Yves Bertot posted to coq semantics theorem-proving by mvermaat on 2008-04-16 15:02:02 as along with 4 people _Anne_ jrw bunge robotact
	A locally nameless solution to the POPLmark challenge [My Copy] (January 2007) by Xavier Leroy posted to bachelor-project compilers coq literature-study poplmark verification by mvermaat on 2008-02-26 14:43:42 as
	A New Extraction for Coq [My Copy] Types for Proofs and Programs (2003), pp. 617-617. by Pierre Letouzey posted to bachelor-project coq functional-programming by mvermaat on 2008-02-26 14:33:05 as along with 2 people msakai jimburton
	Interactive Theorem Proving and Program Development [My Copy] (24 June 2004) by Yves Bertot, Pierre Castéran, Pierre Casttran posted to bachelor-project coq functional-programming verification by mvermaat on 2008-02-26 14:28:45 as along with 2 people jimburton leonardo
	A certified type-preserving compiler from lambda calculus to assembly language [My Copy] SIGPLAN Not., Vol. 42, No. 6. (June 2007), pp. 54-65. by Adam Chlipala posted to bachelor-project compilers coq cps lambda-calculus verification by mvermaat on 2008-02-26 13:46:48 as along with 2 people and 2 groups pedagand jkominek ConcertRG Lambda the Ultimate
	Mechanized Verification of CPS Transformations [My Copy] Logic for Programming, Artificial Intelligence, and Reasoning (2007), pp. 211-225. by Zaynah Dargaye, Xavier Leroy posted to bachelor-project compilers coq cps verification by mvermaat on 2008-02-26 13:39:56 as

Note: You may cite this page as: http://www.citeulike.org/user/mvermaat/tag/coq

CiteULike organises scholarly (or academic) papers or literature and provides bibliographic (which means it makes bibliographies) for universities and higher education establishments. It helps undergraduates and postgraduates. People studying for PhDs or in postdoctoral (postdoc) positions. The service is similar in scope to EndNote or RefWorks or any other reference manager like BibTeX, but it is a social bookmarking service for scientists and humanities researchers.

lambda-calculus	27
bachelor-project	18
binding	16
coq	16
functional-programming	16
literature-study	14
types	13
compilers	12
verification	12
cps	11
logic	8
master-project	8
poplmark	7
rewriting	7
syntax	7
theorem-proving	7
algebra	5
dutch	4
recursion	4
algebraic-specifications	3
coinduction	3
equational-logic	3
infinitary-rewriting	3
normalization	3
redexes	3
rpo	3
semantics	3
termination	3
latex	2
ml	2
nominal	2
parsing	2
proof-theory	2
sdf	2
stratego	2
substitution	2
translation-validation	2
antropology	1
dependent-types	1
dsl	1
isabelle	1
linear-algebra	1
paradox	1
scheme	1
set-theory	1

mvermaat's coq [16 articles] Export

mvermaat's tags