|
1 @inproceedings{HuffmanUrban10, |
|
2 author = {B.~Huffman and C.~Urban}, |
|
3 title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, |
|
4 booktitle = {Proc.~of the 1st Conference on Interactive Theorem Proving (ITP'10)}, |
|
5 pages = {35--50}, |
|
6 volume = {6172}, |
|
7 series = {LNCS}, |
|
8 year = {2010} |
|
9 } |
|
10 @inproceedings{Sac11, |
|
11 author = {Cezary Kaliszyk and |
|
12 Christian Urban}, |
|
13 title = {Quotients revisited for {I}sabelle/{HOL}}, |
|
14 booktitle = {Proc. of the 26th ACM Symposium on Applied Computing (SAC'11)}, |
|
15 year = {2011}, |
|
16 pages = {1639-1644}, |
|
17 publisher = {ACM}, |
|
18 editor = {William C. Chu and W. Eric Wong and Mathew J. Palakal and Chih-Cheng Hung}, |
|
19 } |
|
20 @inproceedings{Esop11, |
|
21 author = {Christian Urban and |
|
22 Cezary Kaliszyk}, |
|
23 title = {General Bindings and Alpha-Equivalence in {N}ominal {I}sabelle}, |
|
24 year = {2011}, |
|
25 pages = {480-500}, |
|
26 booktitle = {Proc. of the 20th European Symposium on Programming (ESOP'11)}, |
|
27 publisher = {Springer Verlag}, |
|
28 series = {LNCS}, |
|
29 volume = {6602}, |
|
30 editor = {Gilles Barthe}, |
|
31 } |
|
32 |
|
33 @book{LambdaBook, |
|
34 author = {Hendrik Pieter Barendregt}, |
|
35 title={{The Lambda Calculus: Its Syntax and Semantics}}, |
|
36 year={2001}, |
|
37 publisher={Elsevier}, |
|
38 volume = {103}, |
|
39 series = {Studies in Logic and the Foundations of Mathematics}, |
|
40 } |
|
41 |
|
42 @article{Pitts03, |
|
43 author = {Andrew M.~Pitts}, |
|
44 title = {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and |
|
45 {B}inding}, |
|
46 journal = {Information and Computation}, |
|
47 year = {2003}, |
|
48 volume = {183}, |
|
49 pages = {165--193} |
|
50 } |
|
51 |
|
52 @Article{Norrish06, |
|
53 author = {Michael Norrish}, |
|
54 title = {Mechanising $\lambda$-Calculus Using a Classical First Order |
|
55 Theory of Terms with Permutations}, |
|
56 journal = {Higher-Order and Symbolic Computation}, |
|
57 year = 2006, |
|
58 volume = 19, |
|
59 pages = {169--195}, |
|
60 doi = {10.1007/s10990-006-8745-7} |
|
61 } |
|
62 |
|
63 @Inproceedings{NominalLambda, |
|
64 author = {Christian Urban}, |
|
65 title = {{Nominal techniques in Isabelle/HOL}}, |
|
66 booktitle = {Proceedings of the 20th International Conference on Automated Deduction (CADE'05)}, |
|
67 year = {2005}, |
|
68 pages = {38--53}, |
|
69 publisher = {Springer} |
|
70 } |
|
71 @article{LocallyNameless, |
|
72 author = {Randy Pollack and Masahiko Sato and Wilmer Ricciotti}, |
|
73 title = {A Canonical Locally Named Representation of Binding}, |
|
74 journal = {Journal of Automated Reasoning}, |
|
75 year = {2011}, |
|
76 } |