doc-src/isac/CTP-userinterfaces.bib
author Andreas Schulhofer <andreas.schulhofer@student.tugraz.at>
Tue, 11 Jan 2011 12:34:12 +0100
branchdecompose-isar
changeset 38100 905c8bfcf39a
parent 38096 4872b10c8747
child 38101 09b428a6b09d
permissions -rw-r--r--
CTP-ui
neuper@38096
     1
@InProceedings{makarius:isa-scala-jedit,
neuper@38096
     2
  author = 	 {Makarius Wenzel},
neuper@38096
     3
  title = 	 {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
neuper@38096
     4
  booktitle = {User Interfaces for Theorem Provers (UITP 2010)},
neuper@38096
     5
  year = 	 {2010},
neuper@38096
     6
  editor = 	 {C. Sacerdoti Coen and D. Aspinall},
neuper@38096
     7
  address = 	 {Edinburgh, Scotland},
neuper@38096
     8
  month = 	 {July},
neuper@38096
     9
  organization = {FLOC 2010 Satellite Workshop},
neuper@38096
    10
  note = 	 {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf}
neuper@38096
    11
}
neuper@38096
    12
neuper@38096
    13
@Book{db:dom-eng,
neuper@38096
    14
  author = 	 {Bj{\o}rner, Dines},
neuper@38096
    15
  title = 	 {Domain Engineering. Technology Management, Research and Engineering},
neuper@38096
    16
  publisher = 	 {JAIST Press},
neuper@38096
    17
  year = 	 {2009},
neuper@38096
    18
  month = 	 {Feb},
neuper@38096
    19
  series = 	 {COE Research Monograph Series},
neuper@38096
    20
  volume = 	 {4},
neuper@38096
    21
  address = 	 {Nomi, Japan}
neuper@38096
    22
}
neuper@38096
    23
neuper@38094
    24
@inproceedings{Haftmann-Nipkow:2010:code,
neuper@38094
    25
  author =      {Florian Haftmann and Tobias Nipkow},
neuper@38094
    26
  title =       {Code Generation via Higher-Order Rewrite Systems},
neuper@38094
    27
  booktitle =   {Functional and Logic Programming, 10th International
neuper@38094
    28
Symposium: {FLOPS} 2010},
neuper@38094
    29
  year =        {2010},
neuper@38094
    30
  publisher =   {Springer},
neuper@38094
    31
  series =      {Lecture Notes in Computer Science},
neuper@38094
    32
  volume =      {6009}
neuper@38094
    33
}
neuper@38094
    34
neuper@38094
    35
@Manual{coq1999,
neuper@38094
    36
  title = 	 {The Coq Proof Assistant},
neuper@38094
    37
  author = 	 {Barras, B. and others},
neuper@38094
    38
  organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},
neuper@38094
    39
  month = 	 {July},
neuper@38094
    40
  year = 	 {1999},
neuper@38094
    41
  pnote={},status={cited},source={mkm01.caprotti},location={}  
neuper@38094
    42
}
neuper@38094
    43
neuper@38094
    44
@Book{meta-ML,
neuper@38094
    45
  author = 	 {Gordon,M. and Milner,R.  and Wadsworth,C. P.},
neuper@38094
    46
  title = 	 {Edinburgh LCF: A Mechanised Logic of Computation},
neuper@38094
    47
  publisher = 	 { Springer-Verlag},
neuper@38094
    48
  year = 	 {1979},
neuper@38094
    49
  volume = 	 {78},
neuper@38094
    50
  series = 	 {Lecture Notes in Computer Science}
neuper@38094
    51
}
neuper@38094
    52
 
neuper@38089
    53
@book{Paulson:Isa94,
neuper@38089
    54
        title={Isabelle: a generic theorem prover}, 
neuper@38089
    55
        author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, 
neuper@38089
    56
	volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, 
neuper@38089
    57
	note={With contributions by Topias Nipkow},
neuper@38089
    58
        status={},source={},location={-} 
neuper@38089
    59
        }  
neuper@38089
    60
neuper@38079
    61
@Book{pl:milner97,
neuper@38079
    62
  author = 	 {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
neuper@38079
    63
  title = 	 {The Definition of Standard ML (Revised)},
neuper@38079
    64
  publisher = 	 {The MIT Press},
neuper@38079
    65
  year = 	 1997,
neuper@38079
    66
  address =	 {Cambridge, London},
neuper@38079
    67
  annote =	 {97bok375}
neuper@38079
    68
}
neuper@38079
    69
neuper@38079
    70
@Article{back-grundy-wright-98,
neuper@38079
    71
  author = 	 {Back, Ralph and Grundy, Jim and von Wright, Joakim},
neuper@38079
    72
  title = 	 {Structured Calculational Proof},
neuper@38079
    73
  journal = 	 {Formal Aspects of Computing},
neuper@38079
    74
  year = 	 {1998},
neuper@38079
    75
  number = 	 {9},
neuper@38079
    76
  pages = 	 {469-483}
neuper@38079
    77
}
neuper@38079
    78
neuper@38079
    79
@Manual{isar-impl,
neuper@38079
    80
  title = 	 {The {Isabelle/Isar} Implementation},
neuper@38079
    81
  author = 	 {Makarius Wenzel},
neuper@38079
    82
  month = 	 {April 19},
neuper@38079
    83
  year = 	 {2009},
neuper@38079
    84
  note = 	 {With contributions by Florian Haftmann and Larry Paulson}
neuper@38079
    85
}
neuper@38079
    86
neuper@38079
    87
@InProceedings{wenzel:isar,
neuper@38079
    88
  author = 	 {Wenzel, Markus},
neuper@38079
    89
  title = 	 {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
neuper@38079
    90
  booktitle = 	 {Theorem Proving in Higher Order Logics},
neuper@38079
    91
  year = 	 {1999},
neuper@38079
    92
  editor = 	 {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},
neuper@38079
    93
  series = 	 {LNCS 1690},
neuper@38079
    94
  organization = {12th International Conference TPHOLs'99},
neuper@38079
    95
  publisher = {Springer}
neuper@38079
    96
}
andreas@38100
    97
andreas@38100
    98