Teaching Algorithms and Data Structures with a Proof Assistant

被引：1
|
作者：
Nipkow, Tobias [1 ]
机构：
[1] Tech Univ Munich, Munich, Germany
来源：
CPP '21: PROCEEDINGS OF THE 10TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS | 2021年
关键词：
Data structures; verification; teaching; Isabelle;
D O I：
10.1145/3437992.3439910
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We report on a new course Verified Functional Data Structures and Algorithms taught at the Technical University of Munich. The course first introduces students to interactive theorem proving with the Isabelle proof assistant. Then it covers a range of standard data structures, in particular search trees and priority queues: it is shown how to express these data structures functionally and how to reason about their correctness and running time in Isabelle.
引用
收藏
页码：1 / 3
页数：3
相关论文
共 50 条
  • [1] Teaching Practice in Algorithms and Data Structures
    Martinez, Cristian A.
    Nocera, Carlos
    Rodriguez, Diego A.
    Orozco, Ismael
    Xamena, Eduardo
    2017 36TH INTERNATIONAL CONFERENCE OF THE CHILEAN COMPUTER SCIENCE SOCIETY (SCCC), 2017,
  • [2] Using randomization in the teaching of data structures and algorithms
    Goodrich, MT
    Tamassia, R
    PROCEEDINGS OF THE THIRTIETH SIGCSE TECHNICAL SYMPOSIUM ON COMPUTER SCIENCE EDUCATION, 1999, : 53 - 57
  • [3] Teaching Reform and Practice of "Algorithms and Data Structures"
    Li, Qing
    Chen, Weiwei
    Tang, Yanqin
    PROCEEDINGS OF THE 2013 CONFERENCE ON EDUCATION TECHNOLOGY AND MANAGEMENT SCIENCE (ICETMS 2013), 2013, : 464 - 468
  • [4] Teaching Data Structures and Algorithms Through Games
    Carneiro, Davide
    Carvalho, Mariana
    METHODOLOGIES AND INTELLIGENT SYSTEMS FOR TECHNOLOGY ENHANCED LEARNING, 2023, 538 : 3 - 12
  • [5] A toolbox to teaching and learning data structures: "Live Algorithms"
    Navarro, PLKG
    INTERNATIONAL CONFERENCE ON EDUCATION AND INFORMATION SYSTEMS: TECHNOLOGIES AND APPLICATIONS, PROCEEDINGS, 2003, : 182 - 184
  • [6] Teaching algorithms and data structures: 10 personal observations
    Bieri, H
    COMPUTER SCIENCE IN PERSPECTIVE: ESSAYS DEDICATED TO THOMAS OTTMANN, 2003, 2598 : 39 - 48
  • [7] Some innovations of teaching the course on Data structures and algorithms
    Steingartner, William
    Eged, Jan
    Radakovic, Davorka
    Novitzka, Valerie
    2019 IEEE 15TH INTERNATIONAL SCIENTIFIC CONFERENCE ON INFORMATICS (INFORMATICS 2019), 2019, : 389 - 395
  • [8] Teaching Software Testing in an Algorithms and Data Structures Course
    Arcuri, Andrea
    2020 IEEE 13TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS (ICSTW), 2020, : 419 - 424
  • [9] Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
    Nipkow, Tobias
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2012, 7148 : 24 - 38
  • [10] Application of Blended Learning in Data Structures and Algorithms Course Teaching
    Liu, Xiaojing
    Wang, Xiaoying
    Wang, Rui
    PROCEEDINGS OF THE 2013 THE INTERNATIONAL CONFERENCE ON EDUCATION TECHNOLOGY AND INFORMATION SYSTEM (ICETIS 2013), 2013, 65 : 1070 - 1074
12345