Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/isac/CTP-userinterfaces.bib
author Walther Neuper <neuper@ist.tugraz.at>
Mon, 10 Jan 2011 12:36:33 +0100
branchdecompose-isar
changeset 38094 f8508fab187c
parent 38089 042b19985ea0
child 38096 4872b10c8747
permissions -rw-r--r--
CTP-gui: new refs 
     1 @inproceedings{Haftmann-Nipkow:2010:code,

     2   author =      {Florian Haftmann and Tobias Nipkow},

     3   title =       {Code Generation via Higher-Order Rewrite Systems},

     4   booktitle =   {Functional and Logic Programming, 10th International

     5 Symposium: {FLOPS} 2010},

     6   year =        {2010},

     7   publisher =   {Springer},

     8   series =      {Lecture Notes in Computer Science},

     9   volume =      {6009}

    10 }

    11 

    12 @InProceedings{wenzel:isar,

    13   author = 	 {Wenzel, Markus},

    14   title = 	 {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},

    15   booktitle = 	 {Theorem Proving in Higher Order Logics},

    16   year = 	 {1999},

    17   editor = 	 {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},

    18   series = 	 {LNCS 1690},

    19   organization = {12th International Conference TPHOLs'99},

    20   publisher = {Springer}

    21 }

    22 

    23 @Manual{coq1999,

    24   title = 	 {The Coq Proof Assistant},

    25   author = 	 {Barras, B. and others},

    26   organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},

    27   month = 	 {July},

    28   year = 	 {1999},

    29   pnote={},status={cited},source={mkm01.caprotti},location={}  

    30 }

    31 

    32 @Book{meta-ML,

    33   author = 	 {Gordon,M. and Milner,R.  and Wadsworth,C. P.},

    34   title = 	 {Edinburgh LCF: A Mechanised Logic of Computation},

    35   publisher = 	 { Springer-Verlag},

    36   year = 	 {1979},

    37   volume = 	 {78},

    38   series = 	 {Lecture Notes in Computer Science}

    39 }

    40  

    41 @book{Paulson:Isa94,

    42         title={Isabelle: a generic theorem prover}, 

    43         author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, 

    44 	volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, 

    45 	note={With contributions by Topias Nipkow},

    46         status={},source={},location={-} 

    47         }  

    48 

    49 @Book{pl:milner97,

    50   author = 	 {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},

    51   title = 	 {The Definition of Standard ML (Revised)},

    52   publisher = 	 {The MIT Press},

    53   year = 	 1997,

    54   address =	 {Cambridge, London},

    55   annote =	 {97bok375}

    56 }

    57 

    58 @Article{back-grundy-wright-98,

    59   author = 	 {Back, Ralph and Grundy, Jim and von Wright, Joakim},

    60   title = 	 {Structured Calculational Proof},

    61   journal = 	 {Formal Aspects of Computing},

    62   year = 	 {1998},

    63   number = 	 {9},

    64   pages = 	 {469-483}

    65 }

    66 

    67 @Manual{isar-impl,

    68   title = 	 {The {Isabelle/Isar} Implementation},

    69   author = 	 {Makarius Wenzel},

    70   month = 	 {April 19},

    71   year = 	 {2009},

    72   note = 	 {With contributions by Florian Haftmann and Larry Paulson}

    73 }

    74 

    75 @InProceedings{wenzel:isar,

    76   author = 	 {Wenzel, Markus},

    77   title = 	 {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},

    78   booktitle = 	 {Theorem Proving in Higher Order Logics},

    79   year = 	 {1999},

    80   editor = 	 {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},

    81   series = 	 {LNCS 1690},

    82   organization = {12th International Conference TPHOLs'99},

    83   publisher = {Springer}

    84 }
wneuper/isa