references.bib

@inproceedings{bertot1991occurrences,
  author = {Bertot, Yves},
  title = {Occurrences in debugger specifications},
  year = {1991},
  isbn = {0897914287},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/113445.113473},
  booktitle = {Proceedings of the ACM SIGPLAN 1991 Conference on Programming
               Language Design and Implementation},
  pages = {327–337},
  numpages = {11},
  location = {Toronto, Ontario, Canada},
  series = {PLDI '91},
}

@article{bernstein1995focusing,
  title = {Operational Semantics of a Focusing Debugger},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {1},
  pages = {13-31},
  year = {1995},
  note = {MFPS XI, Mathematical Foundations of Programming Semantics, Eleventh
          Annual Conference},
  issn = {1571-0661},
  doi = {10.1016/S1571-0661(04)80002-1},
  url = {https://www.sciencedirect.com/science/article/pii/S1571066104800021},
  lastchecked = {2026-05-29},
  author = {Karen L. Bernstein and Eugene W. Stark},
  abstract = {This paper explores two main ideas: (1) a debugger for a
              programming language ought to have a formal semantic definition
              that is closely allied to the formal definition of the language
              itself; and (2) a debugger for very high level programming language
              ought to provide support for exposing hidden information in a
              controlled fashion. We investigate these ideas by giving formal
              semantic definitions for a simple functional programming language
              and an associated debugger for the language. The formal definitions
              are accomplished using structured operational semantics, and they
              demonstrate one way in which the formal definition of a debugger
              might be built “on top of” the formal definition of the underlying
              language. The debugger itself provides the novel capability of
              allowing the programmer to “focus” or shift the scope of attention
              in a syntax-directed fashion to a specific subexpression within the
              program, and to view the execution of the program from that
              vantage. The main formal result about the debugger is that
              “focusing preserves meaning,” in the sense that a program being
              debugged exhibits equivalent (bisimilar) operational behavior
              regardless of the subexpression to which the focus has been
              shifted.},
}

@inproceedings{clements2001stepper,
  author = "Clements, John and Flatt, Matthew and Felleisen, Matthias",
  editor = "Sands, David",
  title = "Modeling an Algebraic Stepper",
  booktitle = "Programming Languages and Systems",
  year = "2001",
  publisher = "Springer Berlin Heidelberg",
  address = "Berlin, Heidelberg",
  pages = "320--334",
  abstract = "Programmers rely on the correctness of the tools in their
              programming environments. In the past, semanticists have studied
              the correctness of compilers and compiler analyses, which are the
              most important tools. In this paper, we make the case that other
              tools, such as debuggers and steppers, deserve semantic models, too
              , and that using these models can help in developing these tools.",
  isbn = "978-3-540-45309-3",
  doi = {10.1007/3-540-45309-1_21},
}

@inproceedings{omar2017hazelnut,
  author = {Omar, Cyrus and Voysey, Ian and Hilton, Michael and Aldrich,
            Jonathan and Hammer, Matthew A.},
  title = {Hazelnut: a bidirectionally typed structure editor calculus},
  year = {2017},
  isbn = {9781450346603},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/3009837.3009900},
  abstract = {Structure editors allow programmers to edit the tree structure of
              a program directly. This can have cognitive benefits, particularly
              for novice and end-user programmers. It also simplifies matters for
              tool designers, because they do not need to contend with malformed
              program text. This paper introduces Hazelnut, a structure editor
              based on a small bidirectionally typed lambda calculus extended
              with holes and a cursor. Hazelnut goes one step beyond syntactic
              well-formedness: its edit actions operate over statically
              meaningful incomplete terms. Na\"{\i}vely, this would force the
              programmer to construct terms in a rigid "outside-in" manner. To
              avoid this problem, the action semantics automatically places terms
              assigned a type that is inconsistent with the expected type inside
              a hole. This meaningfully defers the type consistency check until
              the term inside the hole is finished. Hazelnut is not intended as
              an end-user tool itself. Instead, it serves as a foundational
              account of typed structure editing. To that end, we describe how
              Hazelnut's rich metatheory, which we have mechanized using the Agda
              proof assistant, serves as a guide when we extend the calculus to
              include binary sum types. We also discuss various interpretations
              of holes, and in so doing reveal connections with gradual typing
              and contextual modal type theory, the Curry-Howard interpretation
              of contextual modal logic. Finally, we discuss how Hazelnut's
              semantics lends itself to implementation as an event-based
              functional reactive program. Our simple reference implementation is
              written using js_of_ocaml.},
  booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of
               Programming Languages},
  pages = {86–99},
  numpages = {14},
  keywords = {bidirectional type systems, gradual typing, mechanized metatheory,
              structure editors},
  location = {Paris, France},
  series = {POPL '17},
}

@article{omar2019live,
  author = {Omar, Cyrus and Voysey, Ian and Chugh, Ravi and Hammer, Matthew A.},
  title = {Live functional programming with typed holes},
  year = {2019},
  issue_date = {January 2019},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {3},
  number = {POPL},
  doi = {10.1145/3290327},
  abstract = {Live programming environments aim to provide programmers (and
              sometimes audiences) with continuous feedback about a program's
              dynamic behavior as it is being edited. The problem is that
              programming languages typically assign dynamic meaning only to
              programs that are complete, i.e. syntactically well-formed and free
              of type errors. Consequently, live feedback presented to the
              programmer exhibits temporal or perceptive gaps. This paper
              confronts this "gap problem" from type-theoretic first principles
              by developing a dynamic semantics for incomplete functional
              programs, starting from the static semantics for incomplete
              functional programs developed in recent work on Hazelnut. We model
              incomplete functional programs as expressions with holes, with
              empty holes standing for missing expressions or types, and
              non-empty holes operating as membranes around static and dynamic
              type inconsistencies. Rather than aborting when evaluation
              encounters any of these holes as in some existing systems,
              evaluation proceeds around holes, tracking the closure around each
              hole instance as it flows through the remainder of the program.
              Editor services can use the information in these hole closures to
              help the programmer develop and confirm their mental model of the
              behavior of the complete portions of the program as they decide how
              to fill the remaining holes. Hole closures also enable a
              fill-and-resume operation that avoids the need to restart
              evaluation after edits that amount to hole filling. Formally, the
              semantics borrows machinery from both gradual type theory (which
              supplies the basis for handling unfilled type holes) and contextual
              modal type theory (which supplies a logical basis for hole
              closures), combining these and developing additional machinery
              necessary to continue evaluation past holes while maintaining type
              safety. We have mechanized the metatheory of the core calculus,
              called Hazelnut Live, using the Agda proof assistant. We have also
              implemented these ideas into the Hazel programming environment. The
              implementation inserts holes automatically, following the Hazelnut
              edit action calculus, to guarantee that every editor state has some
              (possibly incomplete) type. Taken together with this paper's type
              safety property, the result is a proof-of-concept live programming
              environment where rich dynamic feedback is truly available without
              gaps, i.e. for every reachable editor state.},
  journal = {Proc. ACM Program. Lang.},
  month = jan,
  articleno = {14},
  numpages = {32},
  keywords = {typed holes, structured editing, live programming, gradual typing,
              contextual modal type theory},
}

@article{paul1994scruple,
  author = {Paul, S. and Prakash, A.},
  title = {A Framework for Source Code Search Using Program Patterns},
  year = {1994},
  issue_date = {June 1994},
  publisher = {IEEE Press},
  volume = {20},
  number = {6},
  issn = {0098-5589},
  doi = {10.1109/32.295894},
  abstract = {For maintainers involved in understanding and reengineering large
              software, locating source code fragments that match certain
              patterns is a critical task. Existing solutions to the problem are
              few, and they either involve manual, painstaking scans of the
              source code using tools based on regular expressions, or the use of
              large, integrated software engineering environments that include
              simple pattern-based query processors in their toolkits. We present
              a framework in which pattern languages are used to specify
              interesting code features. The pattern languages are derived by
              extending the source programming language with pattern-matching
              symbols. We describe SCRUPLE, a finite state machine-based source
              code search tool, that efficiently implements this framework. We
              also present experimental performance results obtained from a
              SCRUPLE prototype, and the user interface of a source code browser
              built on top of SCRUPLE.},
  journal = {IEEE Trans. Softw. Eng.},
  month = jun,
  pages = {463–475},
  numpages = {13},
  keywords = {SCRUPLE, finite state machine, finite state machines, formal
              specification, integrated software engineering environments,
              pattern languages, pattern-based query processors, program patterns
              , programming environments, prototype, query languages, software
              maintenance, software reengineering, software toolkits, software
              tools, software understanding, source code, source code browser,
              source code fragments, source code search, source code search tool,
              source programming language, user interface, user interfaces},
}

@inproceedings{crew1997astlog,
  author = {Crew, Roger F.},
  title = {ASTLOG: a language for examining abstract syntax trees},
  year = {1997},
  publisher = {USENIX Association},
  address = {USA},
  abstract = {We desired a facility for locating/analyzing syntactic artifacts
              in abstract syntax trees of C/C++ programs, similar to the facility
              grep or awk provides for locating artifacts at the lexical level.
              Prolog, with its implicit pattern-matching and backtracking
              capabilities, is a natural choice for such an application. We have
              developed a Prolog variant that avoids the overhead of translating
              the source syntactic structures into the form of a Prolog database;
              this is crucial to obtaining acceptable performance on large
              programs. An interpreter for this language has been implemented and
              used to find various kinds of syntactic bugs and other questionable
              constructs in real programs like Microsoft SQL server (450Klines)
              and Microsoft Word (2Mlines) in time comparable to the runtime of
              the actual compiler.The model in which terms are matched against an
              implicit current object, rather than simply proven against a
              database of facts, leads to a distinct "inside-out functional"
              programming style that is quite unlike typical Prolog, but one that
              is, in fact, well-suited to the examination of trees. Also, various
              second-order Prolog set-predicates may be implemented via
              manipulation of the current object, thus retaining an important
              feature without entailing that the database be dynamically
              extensible as the usual implementation does.},
  booktitle = {Proceedings of the Conference on Domain-Specific Languages on
               Conference on Domain-Specific Languages (DSL), 1997},
  pages = {18},
  numpages = {1},
  location = {Santa Barbara, California},
  series = {DSL'97},
  doi = {10.5555/1267950.1267968},
}

@inproceedings{visser2001stratego,
  author = {Visser, Eelco},
  title = {Stratego: A Language for Program Transformation Based on Rewriting
           Strategies},
  year = {2001},
  isbn = {3540421173},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  booktitle = {Proceedings of the 12th International Conference on Rewriting
               Techniques and Applications},
  pages = {357–362},
  numpages = {6},
  series = {RTA '01},
  doi = {10.1007/3-540-45127-7_27},
}

@article{furukawa2019stepping,
  author = {Furukawa, Tsukino and Cong, Youyou and Asai, Kenichi},
  title = {Stepping OCaml},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = {295},
  pages = {17--34},
  year = {2019},
  doi = {10.4204/EPTCS.295.2},
}

@book{shapiro1983algorithmic,
  author = {Shapiro, Ehud Y.},
  title = {Algorithmic Program Debugging},
  publisher = {The MIT Press},
  year = {1983},
  month = {04},
  abstract = {Productively combines elements of programming languages,
              environments, logic, and inductive inference to produce effective
              debugging aids. Its use of the PROLOG language provides an
              efficient implementation of the debugging algorithms.},
  isbn = {9780262256964},
  doi = {10.7551/mitpress/1192.001.0001},
}


@inproceedings{cong2016stepper,
  author = {Youyou Cong and Kenichi Asai},
  title = {Implementing a stepper using delimited continuations},
  booktitle = {SCSS 2016. 7th International Symposium on Symbolic Computation in
               Software Science},
  editor = {James H. Davenport and Fadoua Ghourabi},
  series = {EPiC Series in Computing},
  volume = {39},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn = {2398-7340},
  url = {https://easychair.org/publications/paper/7qlb},
  lastchecked = {2026-05-29},
  doi = {10.29007/l2wb},
  pages = {42-54},
  year = {2016},
}


@inproceedings{asai2025modules,
  author = {Asai, Kenichi and Akiyama, Hinano},
  title = {Algebraic Stepper for Simple Modules},
  year = {2025},
  isbn = {9798400713507},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/3704253.3706137},
  abstract = {An algebraic stepper is a pedagogical tool for showing the
              intermediate steps of program execution. This paper presents an
              algebraic stepper for OCaml that supports simple modules with
              hierarchical reference to variables (but without functors or
              signature sealing). When we program with modules, we can refer to a
              variable declared in a parent module directly, whereas we need to
              specify a module path to refer to a variable declared in a child
              module. Therefore, when we build the stepper, we attach a level to
              each variable (bound by let statement without in) and use it to
              maintain correct reference regardless of where a variable is used.
              In this paper, we present and formalize our stepper that implements
              delayed substitution of variables, and discuss the interplay
              between the stepper semantics and the level maintenance. We further
              show that the execution in the stepper semantics is consistent with
              the one in the standard small-step semantics. The resulting stepper
              is implemented, supporting most of the basic constructs of OCaml,
              and is used in an introductory OCaml course in the authors'
              institution.},
  booktitle = {Proceedings of the 2025 ACM SIGPLAN International Workshop on
               Partial Evaluation and Program Manipulation},
  pages = {13–29},
  numpages = {17},
  keywords = {Algebraic stepper, Module, OCaml},
  location = {Denver, CO, USA},
  series = {PEPM '25},
}

@inproceedings{ko2004whyline,
  author = {Ko, Amy J. and Myers, Brad A.},
  title = {Designing the whyline: a debugging interface for asking questions
           about program behavior},
  year = {2004},
  isbn = {1581137028},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/985692.985712},
  abstract = {Debugging is still among the most common and costly of programming
              activities. One reason is that current debugging tools do not
              directly support the inquisitive nature of the activity.
              Interrogative Debugging is a new debugging paradigm in which
              programmers can ask why did and even why didn't questions directly
              about their program's runtime failures. The Whyline is a prototype
              Interrogative Debugging interface for the Alice programming
              environment that visualizes answers in terms of runtime events
              directly relevant to a programmer's question. Comparisons of
              identical debugging scenarios from user tests with and without the
              Whyline showed that the Whyline reduced debugging time by nearly a
              factor of 8, and helped programmers complete 40\% more tasks.},
  booktitle = {Proceedings of the SIGCHI Conference on Human Factors in
               Computing Systems},
  pages = {151–158},
  numpages = {8},
  keywords = {program slicing, debugging, Alice},
  location = {Vienna, Austria},
  series = {CHI '04},
}

@inproceedings{khoo2013expositor,
  author = {Khoo, Yit Phang and Foster, Jeffrey S. and Hicks, Michael},
  booktitle = {2013 35th International Conference on Software Engineering (ICSE)
               },
  title = {Expositor: Scriptable time-travel debugging with first-class traces},
  year = {2013},
  volume = {},
  number = {},
  pages = {352-361},
  keywords = {Debugging;Data structures;Optimized production
              technology;Force;Computer bugs;Writing;Programming},
  doi = {10.1109/ICSE.2013.6606581},
}

@article{gill2000hood,
  title = {Debugging Haskell by Observing Intermediate Data Structures},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {41},
  number = {1},
  pages = {1},
  year = {2001},
  note = {2000 ACM SIGPLAN Haskell Workshop (Satellite Event of PLI 2000)},
  issn = {1571-0661},
  doi = {10.1016/S1571-0661(05)80538-9},
  url = {https://www.sciencedirect.com/science/article/pii/S1571066105805389},
  lastchecked = {2026-05-29},
  author = {Gill, Andy},
  abstract = {Haskell has long needed a debugger. Although there has been much
              research into the topic of debugging lazy functional programs, no
              robust tool has yet come from the Haskell community that can help
              debug full Haskell. This paper describes a portable debugger for
              full Haskell, building only on commonly implemented extensions. It
              is based on the concept of observation of intermediate data
              structures, rather than the more traditional stepping and variable
              examination paradigm used by traditional imperative debuggers.},
}

@inproceedings{wallace2001hat,
  booktitle = {2001 ACM SIGPLAN Haskell Workshop},
  title = {Multiple-View Tracing for Haskell: a New Hat},
  month = {September},
  note = {Universiteit Utrecht UU-CS-2001-23. Final proceedings to appear in
          ENTCS 59(2).},
  address = {Firenze, Italy},
  year = {2001},
  editor = {Ralf Hinze},
  author = {Malcolm Wallace and Olaf Chitil and Thorsten Brehm and Colin
            Runciman},
  keywords = {lazy functional language},
  url = {https://kar.kent.ac.uk/13566/},
  lastchecked = {2026-05-29},
  abstract = {Different tracing systems for Haskell give different views of a
              program at work. In practice, several views are complementary and
              can productively be used together. Until now each system has
              generated its own trace, containing only the information needed for
              its particular view. Here we present the design of a trace that can
              serve several views. The trace is generated and written to file as
              the computation proceeds. We have implemented both the generation
              of the trace and several different viewers.},
}

@article{tolmach1995debugger,
  author = {Tolmach, Andrew and Appel, Andrew W.},
  title = {A Debugger for {Standard ML}},
  journal = {Journal of Functional Programming},
  volume = {5},
  number = {2},
  pages = {155--200},
  year = {1995},
  month = apr,
  publisher = {Cambridge University Press},
  doi = {10.1017/S0956796800001313},
}

@inproceedings{marlow2007ghci,
  author = {Marlow, Simon and Iborra, Jos\'{e} and Pope, Bernard and Gill, Andy},
  title = {A lightweight interactive debugger for haskell},
  year = {2007},
  isbn = {9781595936745},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/1291201.1291204},
  abstract = {This paper describes the design and construction of a Haskell
              source-level debugger built into the GHCi interactive environment.
              We have taken a pragmatic approach: the debugger is based on the
              traditional stop-examine-continue model of online debugging, which
              is simple and intuitive, but has traditionally been shunned in the
              context of Haskell because it exposes the lazy evaluation order. We
              argue that this drawback is not as severe as it may seem, and in
              some cases is an advantage.The design focuses on availability: our
              debugger is intended to work on all programs that can be compiled
              with GHC, and without requiring the programmer to jump through
              additional hoops to debug their program. The debugger has a novel
              approach for reconstructing the type of runtime values in a
              polymorphic context. Our implementation is light on complexity, and
              was integrated into GHC without significant upheaval.},
  booktitle = {Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop},
  pages = {13–24},
  numpages = {12},
  keywords = {lazy evaluation, debugging},
  location = {Freiburg, Germany},
  series = {Haskell '07},
}

@inproceedings{padioleau2008coccinelle,
  author = {Padioleau, Yoann and Lawall, Julia and Hansen, Ren\'{e} Rydhof and
            Muller, Gilles},
  title = {Documenting and automating collateral evolutions in linux device
           drivers},
  year = {2008},
  isbn = {9781605580135},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/1352592.1352618},
  abstract = {The internal libraries of Linux are evolving rapidly, to address
              new requirements and improve performance. These evolutions, however
              , entail a massive problem of collateral evolution in Linux device
              drivers: for every change that affects an API, all dependent
              drivers must be updated accordingly. Manually performing such
              collateral evolutions is time-consuming and unreliable, and has
              lead to errors when modifications have not been done
              consistently.In this paper, we present an automatic program
              transformation tool Coccinelle, for documenting and automating
              device driver collateral evolutions. Because Linux programmers are
              accustomed to manipulating program modifications in terms of patch
              files, this tool uses a language based on the patch syntax to
              express transformations, extending patches to semantic patches.
              Coccinelle preserves the coding style of the original driver, as
              would a human programmer.We have evaluated our approach on 62
              representative collateral evolutions that were previously performed
              manually in Linux 2.5 and 2.6. On a test suite of over 5800
              relevant driver files, the semantic patches for these collateral
              evolutions update over 93\% of the files completely. In the
              remaining cases, the user is typically alerted to a partial match
              against the driver code, identifying the files that must be
              considered manually. We have additionally identified over 150
              driver files where the maintainer made an error in performing the
              collateral evolution, but Coccinelle transforms the code correctly.
              Finally, several patches derived from the use of Coccinelle have
              been accepted into the Linux kernel.},
  booktitle = {Proceedings of the 3rd ACM SIGOPS/EuroSys European Conference on
               Computer Systems 2008},
  pages = {247–260},
  numpages = {14},
  keywords = {collateral evolutions, device drivers, domain-specific language,
              linux, program transformation, software evolution},
  location = {Glasgow, Scotland UK},
  series = {Eurosys '08},
}


@inproceedings{faddegon2015hoed,
  author = {Faddegon, Maarten and Chitil, Olaf},
  title = {Algorithmic debugging of real-world haskell programs: deriving
           dependencies from the cost centre stack},
  year = {2015},
  isbn = {9781450334686},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/2737924.2737985},
  abstract = {Existing algorithmic debuggers for Haskell require a
              transformation of all modules in a program, even libraries that the
              user does not want to debug and which may use language features not
              supported by the debugger. This is a pity, because a promising
              approach to debugging is therefore not applicable to many
              real-world programs. We use the cost centre stack from the Glasgow
              Haskell Compiler profiling environment together with runtime value
              observations as provided by the Haskell Object Observation Debugger
              (HOOD) to collect enough information for algorithmic debugging.
              Program annotations are in suspected modules only. With this
              technique algorithmic debugging is applicable to a much larger set
              of Haskell programs. This demonstrates that for functional
              languages in general a simple stack trace extension is useful to
              support tasks such as profiling and debugging.},
  booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming
               Language Design and Implementation},
  pages = {33–42},
  numpages = {10},
  keywords = {tracing, lazy evaluation, algorithmic debugging, Haskell},
  location = {Portland, OR, USA},
  series = {PLDI '15},
}

      

@inproceedings{gissurarson2023csi,
  author = {Gissurarson, Matth\'{\i}as P\'{a}ll and Applis, Leonhard Herbert},
  title = {CSI: Haskell - Tracing Lazy Evaluations in a Functional Language},
  year = {2024},
  isbn = {9798400716317},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/3652561.3652562},
  abstract = {In non-strict languages such as Haskell the execution of
              individual expressions in a program significantly deviates from the
              order in which they appear in the source code. This can make it
              difficult to find bugs related to this deviation, since the
              evaluation of expressions does not occur in the same order as in
              the source code. At the moment, Haskell errors focus on values
              being produced, whereas it is often the case that faults are due to
              values being consumed. For non-strict languages, values involved in
              a bug are often generated immediately prior to the evaluation of
              the buggy code. This creates an opportunity for evaluation traces,
              tracking recently evaluated locations (which can deviate from
              call-order) to help establish the origin of values involved in
              faults. In this paper, we describe an extension of GHC’s Haskell
              Program Coverage with evaluation traces, recording recent
              evaluations in the coverage file, and reporting an evaluation trace
              alongside the call stack on exception. This lets us reconstruct the
              chain of events and locate the origin of faults. As a case study,
              we applied our initial implementation to the nofib-buggy data set
              and found that some runtime errors greatly benefit from trace
              information.},
  booktitle = {Proceedings of the 35th Symposium on Implementation and
               Application of Functional Languages},
  articleno = {1},
  numpages = {13},
  keywords = {Errors, Fault-Localization, Laziness, Tracing},
  location = {Braga, Portugal},
  series = {IFL '23},
}

@article{yuan2023peanut,
  author = {Yuan, Yongwei and Guest, Scott and Griffis, Eric and Potter, Hannah
            and Moon, David and Omar, Cyrus},
  title = {Live Pattern Matching with Typed Holes},
  year = {2023},
  issue_date = {April 2023},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {7},
  number = {OOPSLA1},
  doi = {10.1145/3586048},
  abstract = {Several modern programming systems, including GHC Haskell, Agda,
              Idris, and Hazel, support typed holes. Assigning static and, to
              varying degree, dynamic meaning to programs with holes allows
              program editors and other tools to offer meaningful feedback and
              assistance throughout editing, i.e. in a live manner. Prior work,
              however, has considered only holes appearing in expressions and
              types. This paper considers, from type theoretic and logical first
              principles, the problem of typed pattern holes. We confront two
              main difficulties, (1) statically reasoning about exhaustiveness
              and irredundancy when patterns are not fully known, and (2) live
              evaluation of expressions containing both pattern and expression
              holes. In both cases, this requires reasoning conservatively about
              all possible hole fillings. We develop a typed lambda calculus,
              Peanut, where reasoning about exhaustiveness and redundancy is
              mapped to the problem of deriving first order entailments. We equip
              Peanut with an operational semantics in the style of Hazelnut Live
              that allows us to evaluate around holes in both expressions and
              patterns. We mechanize the metatheory of Peanut in Agda and
              formalize a procedure capable of deciding the necessary
              entailments. Finally, we scale up and implement these mechanisms
              within Hazel, a programming environment for a dialect of Elm that
              automatically inserts holes during editing to provide static and
              dynamic feedback to the programmer in a maximally live manner, i.e.
              for every possible editor state. Hazel is the first maximally live
              environment for a general-purpose functional language.},
  journal = {Proc. ACM Program. Lang.},
  month = apr,
  articleno = {96},
  numpages = {27},
  keywords = {pattern matching, typed holes},
}

@article{zhao2024marking,
  author = {Zhao, Eric and Maroof, Raef and Dukkipati, Anand and Blinn, Andrew
            and Pan, Zhiyi and Omar, Cyrus},
  title = {Total Type Error Localization and Recovery with Holes},
  year = {2024},
  issue_date = {January 2024},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {8},
  number = {POPL},
  doi = {10.1145/3632910},
  abstract = {Type systems typically only define the conditions under which an
              expression is well-typed, leaving ill-typed expressions formally
              meaningless. This approach is insufficient as the basis for
              language servers driving modern programming environments, which are
              expected to recover from simultaneously localized errors and
              continue to provide a variety of downstream semantic services. This
              paper addresses this problem, contributing the first comprehensive
              formal account of total type error localization and recovery: the
              marked lambda calculus. In particular, we define a gradual type
              system for expressions with marked errors, which operate as
              non-empty holes, together with a total procedure for marking
              arbitrary unmarked expressions. We mechanize the metatheory of the
              marked lambda calculus in Agda and implement it, scaled up, as the
              new basis for Hazel, a full-scale live functional programming
              environment with, uniquely, no meaningless editor states.The marked
              lambda calculus is bidirectionally typed, so localization decisions
              are systematically predictable based on a local flow of typing
              information. Constraint-based type inference can bring more distant
              information to bear in discovering inconsistencies but this
              notoriously complicates error localization. We approach this
              problem by deploying constraint solving as a type-hole-filling
              layer atop this gradual bidirectionally typed core. Errors arising
              from inconsistent unification constraints are localized exclusively
              to type and expression holes, i.e., the system identifies
              unfillable holes using a system of traced provenances, rather than
              localized in an ad hoc manner to particular expressions. The user
              can then interactively shift these errors to particular downstream
              expressions by selecting from suggested partially consistent type
              hole fillings, which returns control back to the bidirectional
              system. We implement this type hole inference system in Hazel.},
  journal = {Proc. ACM Program. Lang.},
  month = jan,
  articleno = {68},
  numpages = {28},
  keywords = {type errors, bidirectional typing, gradual typing, type inference},
}

@article{sansom1997profiling,
  author = "Sansom, Patrick M. and {Peyton Jones}, Simon L.",
  title = "Formally Based Profiling for Higher-Order Functional Languages",
  journal = "ACM Transactions on Programming Languages and Systems",
  volume = "19",
  number = "2",
  pages = "334--385",
  year = "1997",
  publisher = "ACM",
  doi = "10.1145/244795.244797",
}

@article{parejaflores2007winhipe,
  author = "Pareja-Flores, Crist{\'o}bal and Urquiza-Fuentes, Jaime and Vel{\'a}zquez-Iturbide, J. {\'A}ngel",
  title = "{WinHIPE}: an {IDE} for functional programming based on rewriting and visualization",
  journal = "ACM SIGPLAN Notices",
  volume = "42",
  number = "3",
  pages = "14--23",
  year = "2007",
  publisher = "ACM",
  doi = "10.1145/1273039.1273042",
}

@inproceedings{olmer2014evaluating,
  author = "Olmer, Tim and Heeren, Bastiaan and Jeuring, Johan",
  title = "Evaluating {Haskell} expressions in a tutoring environment",
  booktitle = "Proceedings 3rd International Workshop on Trends in Functional Programming in Education ({TFPIE} 2014)",
  series = "Electronic Proceedings in Theoretical Computer Science",
  volume = "170",
  pages = "50--66",
  year = "2014",
  eprint = "1412.4879",
  archivePrefix = "arXiv",
}

@inproceedings{chitil2005source,
  author = "Chitil, Olaf",
  title = "Source-Based Trace Exploration",
  booktitle = "Implementation and Application of Functional Languages, {IFL} 2004",
  series = "Lecture Notes in Computer Science",
  volume = "3474",
  pages = "126--141",
  year = "2005",
  publisher = "Springer",
  doi = "10.1007/11431664_8",
}

@article{urquiza2007winhipe,
  author = "Urquiza-Fuentes, Jaime and Vel{\'a}zquez-Iturbide, J. {\'A}ngel",
  title = "An Evaluation of the Effortless Approach to Build Algorithm Animations with {WinHIPE}",
  journal = "Electronic Notes in Theoretical Computer Science",
  volume = "178",
  pages = "3--13",
  year = "2007",
  note = "Proceedings of the 4th International Program Visualization Workshop (PVW 2006)",
  doi = "10.1016/j.entcs.2007.01.038",
}

@inproceedings{faddegon2016hoed,
  author = "Faddegon, Maarten and Chitil, Olaf",
  title = "Lightweight Computation Tree Tracing for Lazy Functional Languages",
  booktitle = "Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation ({PLDI} 2016)",
  publisher = "ACM",
  year = "2016",
  doi = "10.1145/2908080.2908104",
}

@article{gerdes2017askelle,
  author = "Gerdes, Alex and Heeren, Bastiaan and Jeuring, Johan and van Binsbergen, L. Thomas",
  title = "{Ask-Elle}: an Adaptable Programming Tutor for {Haskell} Giving Automated Feedback",
  journal = "International Journal of Artificial Intelligence in Education",
  volume = "27",
  number = "1",
  pages = "65--100",
  year = "2017",
  publisher = "Springer",
  doi = "10.1007/s40593-015-0080-x",
}

@inproceedings{reinke2001ghood,
  author = "Reinke, Claus",
  title = "{GHood}---Graphical Visualisation and Animation of {Haskell} Object Observations",
  booktitle = "Proceedings of the 2001 {ACM} {SIGPLAN} Haskell Workshop",
  series = "Electronic Notes in Theoretical Computer Science",
  volume = "59",
  number = "2",
  year = "2001",
  publisher = "Elsevier",
}

@article{sorva2013review,
  author = "Sorva, Juha and Karavirta, Ville and Malmi, Lauri",
  title = "A Review of Generic Program Visualization Systems for Introductory Programming Education",
  journal = "ACM Transactions on Computing Education",
  volume = "13",
  number = "4",
  articleno = "15",
  numpages = "64",
  year = "2013",
  publisher = "ACM",
  doi = "10.1145/2490822",
}

@inproceedings{clements2022notional,
  author = "Clements, John and Krishnamurthi, Shriram",
  title = "Towards a Notional Machine for Runtime Stacks and Scope: When Stacks Don't Stack Up",
  booktitle = "Proceedings of the 2022 {ACM} Conference on International Computing Education Research ({ICER} 2022)",
  pages = "206--222",
  year = "2022",
  publisher = "ACM",
  doi = "10.1145/3501385.3543961",
}

@article{nilsson1994algorithmic,
  author = "Nilsson, Henrik and Fritzson, Peter",
  title = "Algorithmic debugging for lazy functional languages",
  journal = "Journal of Functional Programming",
  volume = "4",
  number = "3",
  pages = "337--370",
  year = "1994",
  publisher = "Cambridge University Press",
  doi = "10.1017/S0956796800001088",
}

@inproceedings{boothe2000bidirectional,
  author = "Boothe, Bob",
  title = "Efficient Algorithms for Bidirectional Debugging",
  booktitle = "Proceedings of the {ACM} {SIGPLAN} 2000 Conference on Programming Language Design and Implementation ({PLDI} 2000)",
  pages = "299--310",
  year = "2000",
  publisher = "ACM",
  doi = "10.1145/349299.349339",
}

@inproceedings{perera2012explain,
  author = "Perera, Roly and Acar, Umut A. and Cheney, James and Levy, Paul Blain",
  title = "Functional Programs That Explain Their Work",
  booktitle = "Proceedings of the 17th {ACM} {SIGPLAN} International Conference on Functional Programming ({ICFP} 2012)",
  pages = "365--376",
  year = "2012",
  publisher = "ACM",
  doi = "10.1145/2364527.2364579",
}

@incollection{pope2004buddha,
  author = "Pope, Bernard",
  editor = "Vene, Varmo and Uustalu, Tarmo",
  title = "Declarative Debugging with Buddha",
  booktitle = "Advanced Functional Programming",
  series = "Lecture Notes in Computer Science",
  volume = "3622",
  pages = "273--308",
  year = "2005",
  publisher = "Springer",
  doi = "10.1007/11546382_7",
}