mvermaat's library 64 articles Export

	Proving Infinitary Normalization [My Copy] Types for Proofs and Programs In Types for Proofs and Programs (2009), pp. 64-82. by Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Klop, Roel de Vrijer posted to rewriting normalization master-project infinitary-rewriting by mvermaat on 2009-11-09 15:44:24 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
	Variabelenbinding en Substitutie als Algebraïsche Operaties [My Copy] In Liber Amicorum for Roel de Vrijer. Letters and essays dedicated to Roel de Vrijer on the occasion of his 60th birthday. (2009), pp. 191-197. by Piet Rodenburg edited by Jan W. Klop, Vincent van Oostrom, Femke van Raamsdonk posted to substitution literature-study lambda-calculus dutch binding algebraic-specifications by mvermaat on 2009-09-30 15:13:21 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
	Infinitary Normalization [My Copy] In We Will Show Them: Essays in Honour of Dov Gabbay, Vol. 2 (2005), pp. 169-192. by J. W. Klop, R. de Vrijer edited by S. N. Artemov, H. Barringer, A. S. d'Avila Garcez, L. C. Lamb, J. Woods posted to rewriting redexes normalization master-project infinitary-rewriting by mvermaat on 2009-09-30 00:14:24 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
	Refining Reduction in the lambda calculus [My Copy] Journal of Functional Programming, Vol. 5, No. 4. (1996), pp. 637-651. by Fairouz Kamareddine, Rob Nederpelt posted to syntax redexes lambda-calculus cps binding by mvermaat on 2009-09-29 23:45:24 as
	The Lambda Calculus: its Syntax and Semantics [My Copy] Vol. 103 (1984) by H. P. Barendrecht posted to binding functional-programming lambda-calculus literature-study semantics by mvermaat on 2009-04-02 15:19:14 as
	Substitution revisited [My Copy] Theor. Comput. Sci., Vol. 59, No. 3. (August 1988), pp. 317-325. by Allen Stoughton posted to binding lambda-calculus literature-study recursion syntax by mvermaat on 2009-03-03 14:02:02 as
	Toward a general theory of names: binding and scope [My Copy] In MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding (2005), pp. 33-40. by James Cheney posted to binding functional-programming nominal syntax by mvermaat on 2009-02-19 16:29:01 as along with 1 person kavabean
	Scrap your nameplate: (functional pearl) [My Copy] SIGPLAN Not., Vol. 40, No. 9. (September 2005), pp. 180-191. by James Cheney posted to binding functional-programming lambda-calculus nominal syntax by mvermaat on 2009-02-19 15:50:10 as along with 1 person kavabean
	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
	Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem [My Copy] Indagationes Mathematicae (1972), pp. 381-392. by N. G. De Bruijn posted to binding lambda-calculus literature-study by mvermaat on 2009-02-12 17:25:16 as
	Functional Pearl: α-conversion is easy [My Copy] by Thorsten Altenkirch posted to binding functional-programming lambda-calculus literature-study by mvermaat on 2009-02-12 13:10:42 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 binding functional-programming lambda-calculus literature-study by mvermaat on 2009-02-12 13:07:11 as along with 4 people robertjohnsimmons eaubin kavabean msakai
	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
	On understanding types, data abstraction, and polymorphism [My Copy] ACM Computing Surveys, Vol. 17 (1985), pp. 471-522. by Luca Cardelli, Peter Wegner posted to functional-programming lambda-calculus literature-study types by mvermaat on 2009-02-04 14:19:01 as
	An extension of system F with subtyping [My Copy] In Information and Computation, Vol. 109 (1994), pp. 750-770. by Luca Cardelli, Simone Martini, John C. Mitchell, Andre Scedrov posted to equational-logic lambda-calculus literature-study poplmark types by mvermaat on 2009-02-04 14:15:31 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
	Post's functional completeness theorem [My Copy] Notre Dame Journal of Formal Logic, Vol. 31, No. 3. (1990) by F. J. Pelletier, N. M. Martin posted to algebra logic by mvermaat on 2008-09-05 15:06:05 as
	On proving functional incompleteness in symbolic logic classes [My Copy] Notre Dame Journal of Formal Logic, Vol. 29, No. 2. (1988), pp. 235-248. by F. J. Pelletier, W. D. Sharp posted to algebra logic by mvermaat on 2008-09-05 15:03:41 as
	Negation, material equivalence, and conditioned nonconjunction: completeness and duality [My Copy] Notre Dame Journal of Formal Logic, Vol. 18, No. 1. (1977), pp. 140-144. by Gerald J. Massey posted to algebra logic by mvermaat on 2008-09-05 14:58:56 as
	WebDSL: A Case Study in Domain-Specific Language Engineering [My Copy] In Generative and Transformational Techniques in Software Engineering (GTTSE 2007) (2008) by E. Visser edited by R. Laemmel, J. Saraiva, J. Visser posted to compilers dsl functional-programming parsing sdf stratego syntax by mvermaat on 2008-05-11 18:36:08 as
	A Solution to the PoplMark Challenge in Isabelle/HOL [My Copy] (2005) by Stefan Berghofer posted to binding isabelle literature-study ml poplmark theorem-proving types by mvermaat on 2008-04-21 12:16:36 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
	Type Systems [My Copy] In The Computer Science and Engineering Handbook (1997) by Luca Cardelli edited by Allen B. Tucker posted to functional-programming lambda-calculus types by mvermaat on 2008-04-16 16:18:03 as along with 11 people and 2 groups talototo draganigajic rgrig greenrd tautologico amorkan lyongu Bluetulip Leho jimburton zuleger SRG_at_UCD Lambda the Ultimate
	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 Syntactic Approach to Type Soundness [My Copy] Information and Computation, Vol. 115, No. 1. (1994), pp. 38-94. by Andrew K. Wright, Matthias Felleisen posted to proof-theory types by mvermaat on 2008-04-16 14:59:42 as along with 11 people and 2 groups vkp greenrd tautologico bunge tov KarlKlose glaubersp gkuan mcclurmc sclv nominolo SRG_at_UCD Lambda the Ultimate
	A formal treatment of the barendregt variable convention in rule inductions [My Copy] In MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding (2005), pp. 25-32. by Christian Urban, Michael Norrish posted to binding lambda-calculus by mvermaat on 2008-04-16 14:57:50 as
	A New Approach to Abstract Syntax with Variable Binding [My Copy] Journal of the Interest Group in Pure and Applied Logics, Vol. 9 (2) (2001), pp. 157-190. by D. M. Gabbay, J. Woods posted to binding lambda-calculus set-theory by mvermaat on 2008-04-16 14:53:44 as
	The Why of Y [My Copy] SIGPLAN Lisp Pointers, Vol. 2, No. 2. (1988), pp. 15-25. by Richard P. Gabriel posted to lambda-calculus recursion by mvermaat on 2008-03-21 17:20:30 as
	Lambda Calculus [My Copy] (2008) by Femke van Raamsdonk posted to lambda-calculus types by mvermaat on 2008-03-21 17:17:16 as
	Lambda Calculus [My Copy] (1997) by C. H. L. Ong posted to lambda-calculus rewriting by mvermaat on 2008-03-21 17:11:32 as
	Introduction to Lambda Calculus [My Copy] In Aspen\aes Workshop on Implementation of Functional Languages, G\"oteborg (1988) by H. P. Barendregt posted to lambda-calculus rewriting types by mvermaat on 2008-03-21 17:06:21 as along with 17 people and 2 groups GorgeousNicko statistic01 yoriyuki pedagand darinm draganigajic JeffreyPalmer yallop pintman glaubersp robertoalamino biehl namin d23 SamB enochguimond MikolkaMikolka Lambda the Ultimate logics of knowledge
	Parsing techniques: a practical guide [My Copy] (1990) by D. Grune, C. J. H. Jacobs posted to compilers parsing by mvermaat on 2008-03-21 17:02:06 as along with 1 person markusd
	The Blind Spot [My Copy] (16 January 2006) by Jean-Yves Girard posted to logic proof-theory types by mvermaat on 2008-03-21 16:54:38 as
	Verifying a CPS Transformation [My Copy] (February 2008) by Martijn Vermaat posted to bachelor-project compilers cps lambda-calculus verification by mvermaat on 2008-03-21 16:42:13 as
	Equationele Specificatie van Datatypen [My Copy] (2008) by Roel de Vrijer, Yde Venema posted to algebraic-specifications equational-logic by mvermaat on 2008-03-21 16:36:10 as
	Algebraic Preliminaries [My Copy] In Algebraic Foundations of Systems Specification (1999) by Donald Sannella, Andrzej Tarlecki edited by Egidio Astesiano, Hans-Joerg Kreowski, Bernd Krieg-Brueckner posted to algebraic-specifications equational-logic by mvermaat on 2008-03-21 16:31:12 as along with 1 person mishra_satish
	Elements of Abstract and Linear Algebra [My Copy] (20 March 2004) by Edwin H. Connell posted to algebra linear-algebra by mvermaat on 2008-03-21 16:18:56 as
	Church’s Thesis and Functional Programming [My Copy] In Church's Thesis After 70 Years (28 February 2007), pp. 518-544. by David Turner edited by Adam Olszewski, Jan Wolenski, Robert Janusz posted to functional-programming lambda-calculus by mvermaat on 2008-03-21 16:09:49 as along with 2 people badi bunge
	Algebra en Computers [My Copy] (2002) by J. Top posted to algebra dutch by mvermaat on 2008-03-21 16:02:32 as
	The not so Short Introduction to LaTeX [My Copy] (February 2008) by Tobias Oetiker posted to latex by mvermaat on 2008-03-21 15:55:45 as
	Handleiding LaTeX [My Copy] (December 1996) by Piet van Oostrom posted to dutch latex by mvermaat on 2008-03-21 15:44:57 as
	Exercises in Free Syntax. Syntax Definition, Parsing, and Assimilation of Language Conglomerates [My Copy] (January 2008) by Martin Bravenboer posted to compilers sdf stratego syntax by mvermaat on 2008-02-26 15:19:11 as
	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
	Translation Validation [My Copy] Lecture Notes in Computer Science, Vol. 1384 (1998) by A. Pnueli, M. Siegel, E. Singerman posted to bachelor-project compilers translation-validation verification by mvermaat on 2008-02-26 14:39:10 as
	Translation validation for an optimizing compiler [My Copy] ACM SIG\-PLAN Notices, Vol. 35, No. 5. (2000), pp. 83-94. by George C. Necula posted to bachelor-project compilers translation-validation verification by mvermaat on 2008-02-26 14:38:17 as

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

Result page: 1 2 Next

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

mvermaat's library 64 articles Export

mvermaat's tags