Eintrag weiter verarbeiten
Online-Ressource

Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings

Gespeichert in:

Personen und Körperschaften: Gonthier, Georges (VerfasserIn), Norrish, Michael (HerausgeberIn)
Titel: Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings/ edited by Georges Gonthier, Michael Norrish
Format: E-Book Konferenzbericht
Sprache: Englisch
veröffentlicht:
Cham [u.a.] Springer 2013
Gesamtaufnahme: SpringerLink
Lecture notes in computer science ; 8307
Schlagwörter:
Logic design
Algebra > Data processing
Computer science
Artificial intelligence
Computer Science
Compilers (Computer programs).
Machine theory.
Konferenzschrift
Druckausg.: Certified programs and proofs, Cham [u.a.] : Springer, 2013, XII, 307 S.
Quelle: Verbunddaten SWB
Zugangsinformationen: Elektronischer Volltext - Campuslizenz
LEADER 07586cam a22014412 4500
001 0-1653173467
003 DE-627
005 20240122104827.0
007 cr uuu---uuuuu
008 140110s2013 gw |||||o 00| ||eng c
020 |a 9783319035451  |9 978-3-319-03545-1 
024 7 |a 10.1007/978-3-319-03545-1  |2 doi 
035 |a (DE-627)1653173467 
035 |a (DE-576)399527710 
035 |a (DE-599)BSZ399527710 
035 |a (OCoLC)867052084 
035 |a (ZBM)1298.68028 
035 |a (ZBM)1298.68028 
035 |a (DE-He213)978-3-319-03545-1 
035 |a (EBP)040552470 
040 |a DE-627  |b ger  |c DE-627  |e rakwb 
041 |a eng 
044 |c XA-DE  |c XA-CH 
050 0 |a QA76.9.L63  |a QA76.5913  |a QA76.63 
050 0 |a QA76.9.L63 
050 0 |a QA76.5913 
050 0 |a QA76.63 
072 7 |a UM  |2 bicssc 
072 7 |a UYF  |2 bicssc 
072 7 |a COM036000  |2 bisacsh 
072 7 |a COM051000  |2 bisacsh 
072 7 |a UYA  |2 bicssc 
084 |a SS 4800  |q BVB  |2 rvk  |0 (DE-625)rvk/143528: 
084 |a *68-06  |2 msc 
084 |a 68N30  |2 msc 
084 |a 68T15  |2 msc 
084 |a 00B25  |2 msc 
084 |a 54.10  |2 bkl 
084 |a 54.71  |2 bkl 
084 |a 54.51  |2 bkl 
100 1 |a Gonthier, Georges  |4 aut 
245 1 0 |a Certified Programs and Proofs  |b Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings  |c edited by Georges Gonthier, Michael Norrish 
264 1 |a Cham [u.a.]  |b Springer  |c 2013 
300 |a Online-Ressource (XII, 309 p. 44 illus, online resource) 
336 |a Text  |b txt  |2 rdacontent 
337 |a Computermedien  |b c  |2 rdamedia 
338 |a Online-Ressource  |b cr  |2 rdacarrier 
490 1 |a Lecture Notes in Computer Science  |v 8307 
490 0 |a SpringerLink  |a Bücher 
500 |a Literaturangaben 
505 8 0 |a Invited Lecturesπn(Sn) in Homotopy Type Theory -- Session 1: Code Verification -- Mostly Sound Type System Improves a Foundational Program Verifier -- Computational Verification of Network Programs in Coq -- Aliasing Restrictions of C11 Formalized in Coq -- Session 2: Elegant Proofs -- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code -- A Constructive Theory of Regular Languages in Coq -- Certified Parsing of Regular Languages -- Session 3: Proof Libraries -- Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL -- Refinements for Free! -- Session 4: Mathematics -- A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem -- Certified Kruskal’s Tree Theorem -- Extracting Proofs from Tabled Proof Search -- Session 5: Certified Transformations -- Formalizing the SAFECode Type System -- Certifiably Sound Parallelizing Transformations -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax -- Session 6: Security -- Formalizing Probabilistic Noninterference -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties -- A Formal Model and Correctness Proof for an Access Control Policy Framework. 
520 |a This book constitutes the refereed proceedings of the Third International Conference on Certified Programs and Proofs, CPP 2013, colocated with APLAS 2013 held in Melbourne, Australia, in December 2013. The 18 revised regular papers presented together with 1 invited lecture were carefully reviewed and selected from 39 submissions. The papers are organized in topical sections on code verification, elegant proofs, proof libraries, certified transformations and security 
650 0 |a Logic design 
650 0 |a Algebra  |x Data processing 
650 0 |a Computer science 
650 0 |a Logic design 
650 0 |a Algebra  |x Data processing 
650 0 |a Artificial intelligence 
650 0 |a Computer science 
650 0 |a Artificial intelligence 
650 0 |a Computer Science 
650 0 |a Compilers (Computer programs). 
650 0 |a Machine theory. 
655 7 |a Konferenzschrift  |0 (DE-588)1071861417  |0 (DE-627)826484824  |0 (DE-576)433375485  |2 gnd-content 
689 0 0 |D s  |0 (DE-588)4135576-3  |0 (DE-627)10566409X  |0 (DE-576)209661925  |a Programmverifikation  |2 gnd 
689 0 1 |D s  |0 (DE-588)4299725-2  |0 (DE-627)104118490  |0 (DE-576)211020982  |a Formale Spezifikationstechnik  |2 gnd 
689 0 2 |D s  |0 (DE-588)4623348-9  |0 (DE-627)327700408  |0 (DE-576)214380408  |a Typprüfung  |2 gnd 
689 0 3 |D s  |0 (DE-588)4069034-9  |0 (DE-627)106104462  |0 (DE-576)209175370  |a Automatisches Beweisverfahren  |2 gnd 
689 0 |5 DE-101 
700 1 |a Norrish, Michael  |e Hrsg.  |4 edt 
776 1 |z 9783319035444 
776 0 8 |i Druckausg.  |z 978-331-90354-4-4 
776 0 8 |i Druckausg.  |t Certified programs and proofs  |d Cham [u.a.] : Springer, 2013  |h XII, 307 S.  |w (DE-627)774437391  |w (DE-576)977443739X  |z 9783319035444 
830 0 |a Lecture notes in computer science  |v 8307  |9 8307  |w (DE-627)316228877  |w (DE-576)093890923  |w (DE-600)2018930-8  |x 1611-3349  |7 ns 
856 4 0 |u https://doi.org/10.1007/978-3-319-03545-1  |m X:SPRINGER  |x Verlag  |z lizenzpflichtig  |3 Volltext 
856 4 0 |u http://dx.doi.org/10.1007/978-3-319-03545-1  |x Resolving-System  |z lizenzpflichtig  |3 Volltext 
856 4 2 |u https://swbplus.bsz-bw.de/bsz399527710cov.jpg  |m V:DE-576  |m X:springer  |q image/jpeg  |v 20150320111425  |3 Cover 
856 4 2 |u https://zbmath.org/?q=an:1298.68028  |m B:ZBM  |v 2021-04-12  |x Verlag  |y Zentralblatt MATH  |3 Inhaltstext 
889 |w (DE-627)77557869X 
912 |a ZDB-2-LNC  |b 2013 
912 |a ZDB-2-SCS  |b 2013 
912 |a ZDB-2-SEB 
912 |a ZDB-2-SXCS  |b 2013 
912 |a ZDB-2-SEB  |b 2013 
935 |h GBV  |i ExPruef 
936 r v |a SS 4800  |b Lecture notes in computer science  |k Informatik  |k Enzyklopädien und Handbücher. Kongressberichte Schriftenreihe. Tafeln und Formelsammlungen  |k Schriftenreihen (indiv. Sign.)  |k Lecture notes in computer science  |0 (DE-627)1271461242  |0 (DE-625)rvk/143528:  |0 (DE-576)201461242 
936 b k |a 54.10  |j Theoretische Informatik  |0 (DE-627)106418815 
936 b k |a 54.71  |j Logikprogrammierung  |0 (DE-627)106418912 
936 b k |a 54.51  |j Programmiermethodik  |0 (DE-627)106418122 
951 |a BO 
950 |a Spezifikationstechnik 
950 |a Formale Methode 
950 |a Formale Beschreibungstechnik 
950 |a Algebraische Spezifikation 
950 |a Verifikation 
950 |a Hoare-Logik 
950 |a Beweis 
950 |a Automatisierung 
950 |a Maschinelles Beweisverfahren 
950 |a Mechanisches Beweisverfahren 
950 |a Theorembeweisen 
950 |a Automatisches Theorembeweisen 
950 |a Automated theorem proving 
950 |a Automatic theorem proving 
950 |a Automatisches Beweisen 
950 |a Theorem 
950 |a Beweissystem 
950 |a Автоматическое доказательство 
950 |a Type checking 
950 |a Typüberprüfung 
950 |a Prüfung 
856 4 0 |u http://dx.doi.org/10.1007/978-3-319-03545-1  |9 DE-14 
852 |a DE-14  |x epn:3363520085  |z 2014-01-10T12:34:13Z 
856 4 0 |u http://dx.doi.org/10.1007/978-3-319-03545-1  |9 DE-15 
852 |a DE-15  |x epn:3363520115  |z 2014-01-10T12:34:14Z 
856 4 0 |u http://dx.doi.org/10.1007/978-3-319-03545-1  |9 DE-Ch1 
852 |a DE-Ch1  |x epn:3363520158  |z 2014-01-10T12:34:13Z 
976 |h Elektronischer Volltext - Campuslizenz 
856 4 0 |u http://dx.doi.org/10.1007/978-3-319-03545-1  |z Zum Online-Dokument  |9 DE-Zi4 
852 |a DE-Zi4  |x epn:3363520182  |z 2014-01-10T12:34:13Z 
856 4 0 |u http://dx.doi.org/10.1007/978-3-319-03545-1  |9 DE-520 
852 |a DE-520  |x epn:3363520212  |z 2014-01-10T12:34:13Z 
980 |a 1653173467  |b 0  |k 1653173467  |o 399527710 
openURL url_ver=Z39.88-2004&ctx_ver=Z39.88-2004&ctx_enc=info%3Aofi%2Fenc%3AUTF-8&rfr_id=info%3Asid%2Fvufind.svn.sourceforge.net%3Agenerator&rft.title=Certified+Programs+and+Proofs%3A+Third+International+Conference%2C+CPP+2013%2C+Melbourne%2C+VIC%2C+Australia%2C+December+11-13%2C+2013%2C+Proceedings&rft.date=2013&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Certified+Programs+and+Proofs%3A+Third+International+Conference%2C+CPP+2013%2C+Melbourne%2C+VIC%2C+Australia%2C+December+11-13%2C+2013%2C+Proceedings&rft.series=Lecture+notes+in+computer+science%2C+8307&rft.au=Gonthier%2C+Georges&rft.pub=Springer&rft.edition=&rft.isbn=3319035452
SOLR
_version_ 1792258642468143104
access_facet Electronic Resources
author Gonthier, Georges
author2 Norrish, Michael
author2_role edt
author2_variant m n mn
author_facet Gonthier, Georges, Norrish, Michael
author_role aut
author_sort Gonthier, Georges
author_variant g g gg
callnumber-first Q - Science
callnumber-label QA76
callnumber-raw QA76.9.L63 QA76.5913 QA76.63, QA76.9.L63, QA76.5913, QA76.63
callnumber-search QA76.9.L63 QA76.5913 QA76.63, QA76.9.L63, QA76.5913, QA76.63
callnumber-sort QA 276.9 L63 Q A76 45913 Q A76 263
callnumber-subject QA - Mathematics
collection ZDB-2-LNC, ZDB-2-SCS, ZDB-2-SEB, ZDB-2-SXCS
contents Invited Lecturesπn(Sn) in Homotopy Type Theory -- Session 1: Code Verification -- Mostly Sound Type System Improves a Foundational Program Verifier -- Computational Verification of Network Programs in Coq -- Aliasing Restrictions of C11 Formalized in Coq -- Session 2: Elegant Proofs -- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code -- A Constructive Theory of Regular Languages in Coq -- Certified Parsing of Regular Languages -- Session 3: Proof Libraries -- Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL -- Refinements for Free! -- Session 4: Mathematics -- A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem -- Certified Kruskal’s Tree Theorem -- Extracting Proofs from Tabled Proof Search -- Session 5: Certified Transformations -- Formalizing the SAFECode Type System -- Certifiably Sound Parallelizing Transformations -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax -- Session 6: Security -- Formalizing Probabilistic Noninterference -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties -- A Formal Model and Correctness Proof for an Access Control Policy Framework., This book constitutes the refereed proceedings of the Third International Conference on Certified Programs and Proofs, CPP 2013, colocated with APLAS 2013 held in Melbourne, Australia, in December 2013. The 18 revised regular papers presented together with 1 invited lecture were carefully reviewed and selected from 39 submissions. The papers are organized in topical sections on code verification, elegant proofs, proof libraries, certified transformations and security
ctrlnum (DE-627)1653173467, (DE-576)399527710, (DE-599)BSZ399527710, (OCoLC)867052084, (ZBM)1298.68028, (DE-He213)978-3-319-03545-1, (EBP)040552470
de15_date 2014-01-10T12:34:14Z
dech1_date 2014-01-10T12:34:13Z
doi_str_mv 10.1007/978-3-319-03545-1
facet_912a ZDB-2-LNC, ZDB-2-SCS, ZDB-2-SEB, ZDB-2-SXCS
facet_avail Online
facet_local_del330 Programmverifikation, Formale Spezifikationstechnik, Typprüfung, Automatisches Beweisverfahren
finc_class_facet Informatik, Mathematik
fincclass_txtF_mv science-computerscience
footnote Literaturangaben
format eBook, ConferenceProceedings
format_access_txtF_mv Book, E-Book
format_de105 Ebook
format_de14 Book, E-Book
format_de15 Book, E-Book
format_del152 Buch
format_detail_txtF_mv text-online-monograph-independent-conference
format_dezi4 e-Book
format_finc Book, E-Book
format_legacy ElectronicBook
format_legacy_nrw Book, E-Book
format_nrw Book, E-Book
format_strict_txtF_mv E-Book
genre Konferenzschrift (DE-588)1071861417 (DE-627)826484824 (DE-576)433375485 gnd-content
genre_facet Konferenzschrift
geogr_code not assigned
geogr_code_person not assigned
hierarchy_parent_id 0-316228877
hierarchy_parent_title Lecture notes in computer science
hierarchy_sequence 8307
hierarchy_top_id 0-316228877
hierarchy_top_title Lecture notes in computer science
id 0-1653173467
illustrated Not Illustrated
imprint Cham [u.a.], Springer, 2013
imprint_str_mv Cham [u.a.]: Springer, 2013
institution DE-14, DE-Zi4, DE-Ch1, DE-520, DE-15
is_hierarchy_id 0-1653173467
is_hierarchy_title Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings
isbn 9783319035451
isbn_isn_mv 9783319035444, 978-331-90354-4-4
issn_isn_mv 1611-3349
kxp_id_str 1653173467
language English
last_indexed 2024-02-29T18:23:53.039Z
local_heading_facet_dezwi2 Logic design, Algebra, Computer science, Artificial intelligence, Computer Science, Compilers (Computer programs)., Machine theory., Data processing, Programmverifikation, Formale Spezifikationstechnik, Typprüfung, Automatisches Beweisverfahren
marc024a_ct_mv 10.1007/978-3-319-03545-1
match_str gonthier2013certifiedprogramsandproofsthirdinternationalconferencecpp2013melbournevicaustraliadecember11132013proceedings
mega_collection Verbunddaten SWB
multipart_link 093890923
multipart_part (093890923)8307
oclc_num 867052084
physical Online-Ressource (XII, 309 p. 44 illus, online resource)
publishDate 2013
publishDateSort 2013
publishPlace Cham [u.a.]
publisher Springer
record_format marcfinc
record_id 399527710
recordtype marcfinc
rsn_id_str_mv (DE-15)3275929
rvk_facet SS 4800
rvk_label Informatik, Enzyklopädien und Handbücher. Kongressberichte Schriftenreihe. Tafeln und Formelsammlungen, Schriftenreihen (indiv. Sign.), Lecture notes in computer science
rvk_path SS, SQ - SU, SS 4000 - SS 5999, SS 4800
rvk_path_str_mv SS, SQ - SU, SS 4000 - SS 5999, SS 4800
series Lecture notes in computer science, 8307
series2 Lecture Notes in Computer Science ; 8307, SpringerLink ; Bücher
source_id 0
spelling Gonthier, Georges aut, Certified Programs and Proofs Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings edited by Georges Gonthier, Michael Norrish, Cham [u.a.] Springer 2013, Online-Ressource (XII, 309 p. 44 illus, online resource), Text txt rdacontent, Computermedien c rdamedia, Online-Ressource cr rdacarrier, Lecture Notes in Computer Science 8307, SpringerLink Bücher, Literaturangaben, Invited Lecturesπn(Sn) in Homotopy Type Theory -- Session 1: Code Verification -- Mostly Sound Type System Improves a Foundational Program Verifier -- Computational Verification of Network Programs in Coq -- Aliasing Restrictions of C11 Formalized in Coq -- Session 2: Elegant Proofs -- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code -- A Constructive Theory of Regular Languages in Coq -- Certified Parsing of Regular Languages -- Session 3: Proof Libraries -- Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL -- Refinements for Free! -- Session 4: Mathematics -- A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem -- Certified Kruskal’s Tree Theorem -- Extracting Proofs from Tabled Proof Search -- Session 5: Certified Transformations -- Formalizing the SAFECode Type System -- Certifiably Sound Parallelizing Transformations -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax -- Session 6: Security -- Formalizing Probabilistic Noninterference -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties -- A Formal Model and Correctness Proof for an Access Control Policy Framework., This book constitutes the refereed proceedings of the Third International Conference on Certified Programs and Proofs, CPP 2013, colocated with APLAS 2013 held in Melbourne, Australia, in December 2013. The 18 revised regular papers presented together with 1 invited lecture were carefully reviewed and selected from 39 submissions. The papers are organized in topical sections on code verification, elegant proofs, proof libraries, certified transformations and security, Logic design, Algebra Data processing, Computer science, Artificial intelligence, Computer Science, Compilers (Computer programs)., Machine theory., Konferenzschrift (DE-588)1071861417 (DE-627)826484824 (DE-576)433375485 gnd-content, s (DE-588)4135576-3 (DE-627)10566409X (DE-576)209661925 Programmverifikation gnd, s (DE-588)4299725-2 (DE-627)104118490 (DE-576)211020982 Formale Spezifikationstechnik gnd, s (DE-588)4623348-9 (DE-627)327700408 (DE-576)214380408 Typprüfung gnd, s (DE-588)4069034-9 (DE-627)106104462 (DE-576)209175370 Automatisches Beweisverfahren gnd, DE-101, Norrish, Michael Hrsg. edt, 9783319035444, Druckausg. 978-331-90354-4-4, Druckausg. Certified programs and proofs Cham [u.a.] : Springer, 2013 XII, 307 S. (DE-627)774437391 (DE-576)977443739X 9783319035444, Lecture notes in computer science 8307 8307 (DE-627)316228877 (DE-576)093890923 (DE-600)2018930-8 1611-3349 ns, https://doi.org/10.1007/978-3-319-03545-1 X:SPRINGER Verlag lizenzpflichtig Volltext, http://dx.doi.org/10.1007/978-3-319-03545-1 Resolving-System lizenzpflichtig Volltext, https://swbplus.bsz-bw.de/bsz399527710cov.jpg V:DE-576 X:springer image/jpeg 20150320111425 Cover, https://zbmath.org/?q=an:1298.68028 B:ZBM 2021-04-12 Verlag Zentralblatt MATH Inhaltstext, (DE-627)77557869X, http://dx.doi.org/10.1007/978-3-319-03545-1 DE-14, DE-14 epn:3363520085 2014-01-10T12:34:13Z, http://dx.doi.org/10.1007/978-3-319-03545-1 DE-15, DE-15 epn:3363520115 2014-01-10T12:34:14Z, http://dx.doi.org/10.1007/978-3-319-03545-1 DE-Ch1, DE-Ch1 epn:3363520158 2014-01-10T12:34:13Z, http://dx.doi.org/10.1007/978-3-319-03545-1 Zum Online-Dokument DE-Zi4, DE-Zi4 epn:3363520182 2014-01-10T12:34:13Z, http://dx.doi.org/10.1007/978-3-319-03545-1 DE-520, DE-520 epn:3363520212 2014-01-10T12:34:13Z
spellingShingle Gonthier, Georges, Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, Lecture notes in computer science, 8307, Invited Lecturesπn(Sn) in Homotopy Type Theory -- Session 1: Code Verification -- Mostly Sound Type System Improves a Foundational Program Verifier -- Computational Verification of Network Programs in Coq -- Aliasing Restrictions of C11 Formalized in Coq -- Session 2: Elegant Proofs -- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code -- A Constructive Theory of Regular Languages in Coq -- Certified Parsing of Regular Languages -- Session 3: Proof Libraries -- Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL -- Refinements for Free! -- Session 4: Mathematics -- A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem -- Certified Kruskal’s Tree Theorem -- Extracting Proofs from Tabled Proof Search -- Session 5: Certified Transformations -- Formalizing the SAFECode Type System -- Certifiably Sound Parallelizing Transformations -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax -- Session 6: Security -- Formalizing Probabilistic Noninterference -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties -- A Formal Model and Correctness Proof for an Access Control Policy Framework., This book constitutes the refereed proceedings of the Third International Conference on Certified Programs and Proofs, CPP 2013, colocated with APLAS 2013 held in Melbourne, Australia, in December 2013. The 18 revised regular papers presented together with 1 invited lecture were carefully reviewed and selected from 39 submissions. The papers are organized in topical sections on code verification, elegant proofs, proof libraries, certified transformations and security, Logic design, Algebra Data processing, Computer science, Artificial intelligence, Computer Science, Compilers (Computer programs)., Machine theory., Konferenzschrift, Programmverifikation, Formale Spezifikationstechnik, Typprüfung, Automatisches Beweisverfahren
swb_id_str 399527710
title Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings
title_auth Certified Programs and Proofs Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings
title_full Certified Programs and Proofs Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings edited by Georges Gonthier, Michael Norrish
title_fullStr Certified Programs and Proofs Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings edited by Georges Gonthier, Michael Norrish
title_full_unstemmed Certified Programs and Proofs Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings edited by Georges Gonthier, Michael Norrish
title_in_hierarchy 8307. Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings (2013)
title_short Certified Programs and Proofs
title_sort certified programs and proofs third international conference cpp 2013 melbourne vic australia december 11 13 2013 proceedings
title_sub Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings
title_unstemmed Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings
topic Logic design, Algebra Data processing, Computer science, Artificial intelligence, Computer Science, Compilers (Computer programs)., Machine theory., Konferenzschrift, Programmverifikation, Formale Spezifikationstechnik, Typprüfung, Automatisches Beweisverfahren
topic_facet Logic design, Algebra, Computer science, Artificial intelligence, Computer Science, Compilers (Computer programs)., Machine theory., Data processing, Konferenzschrift, Programmverifikation, Formale Spezifikationstechnik, Typprüfung, Automatisches Beweisverfahren
url https://doi.org/10.1007/978-3-319-03545-1, http://dx.doi.org/10.1007/978-3-319-03545-1, https://swbplus.bsz-bw.de/bsz399527710cov.jpg, https://zbmath.org/?q=an:1298.68028