src/Doc/Prog_Prove/document/root.bib
author wenzelm
Sat, 01 Jun 2019 11:29:59 +0200
changeset 70299 83774d669b51
parent 68649 f849fc1cb65e
permissions -rw-r--r--
Added tag Isabelle2019-RC4 for changeset ad2d84c42380
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     1
@string{CUP="Cambridge University Press"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     2
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
65348
b5ce7100ddc8 added chains of (in)equations
nipkow
parents: 59317
diff changeset
     3
@string{Springer="Springer"}
b5ce7100ddc8 added chains of (in)equations
nipkow
parents: 59317
diff changeset
     4
b5ce7100ddc8 added chains of (in)equations
nipkow
parents: 59317
diff changeset
     5
@InProceedings{BauerW-TPHOLs01,author={Gertrud Bauer and Markus Wenzel},
b5ce7100ddc8 added chains of (in)equations
nipkow
parents: 59317
diff changeset
     6
title={Calculational Reasoning Revisited --- An {Isabelle/Isar} Experience},
b5ce7100ddc8 added chains of (in)equations
nipkow
parents: 59317
diff changeset
     7
booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001},
b5ce7100ddc8 added chains of (in)equations
nipkow
parents: 59317
diff changeset
     8
editor={R. Boulton and P. Jackson},
b5ce7100ddc8 added chains of (in)equations
nipkow
parents: 59317
diff changeset
     9
year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
@book{HuthRyan,author="Michael Huth and Mark Ryan",
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
title={Logic in Computer Science},publisher=CUP,year=2004}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
@manual{Krauss,author={Alexander Krauss},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
title={Defining Recursive Functions in Isabelle/HOL},
68649
f849fc1cb65e prefer HTTPS;
wenzelm
parents: 65348
diff changeset
    16
note={\url{https://isabelle.in.tum.de/doc/functions.pdf}}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
51784
89fb9f4abf84 more funs
nipkow
parents: 48985
diff changeset
    18
@manual{Nipkow-Main,author={Tobias Nipkow},title={What's in Main},
68649
f849fc1cb65e prefer HTTPS;
wenzelm
parents: 65348
diff changeset
    19
note={\url{https://isabelle.in.tum.de/doc/main.pdf}}}
51784
89fb9f4abf84 more funs
nipkow
parents: 48985
diff changeset
    20
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
publisher=Springer,series=LNCS,volume=2283,year=2002}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
52782
b11d73dbfb76 tuned intro
nipkow
parents: 51784
diff changeset
    25
@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
59317
4ae9d8842597 updated bibtex
nipkow
parents: 57845
diff changeset
    26
title="Concrete Semantics with Isabelle/HOL",publisher="Springer",year=2014,
4ae9d8842597 updated bibtex
nipkow
parents: 57845
diff changeset
    27
note={298 pp. \url{http://concrete-semantics.org}}}
52782
b11d73dbfb76 tuned intro
nipkow
parents: 51784
diff changeset
    28
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
@manual{IsarRef,author={Makarius Wenzel},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
title={The Isabelle/Isar Reference Manual},
68649
f849fc1cb65e prefer HTTPS;
wenzelm
parents: 65348
diff changeset
    31
note={\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}