More Like this

1. A formalization of Java’s concurrent access modes

   https://doi.org/10.1145/3360568  

   Bender, John; Palsberg, Jens (October 2019, Proceedings of the ACM on Programming Languages)
2. A Formalization of Core Why3 in Coq

   https://doi.org/10.1145/3632902  

   Cohen, Joshua_M; Johnson-Freyd, Philip (January 2024, Proceedings of the ACM on Programming Languages)

   Intermediate verification languages like Why3 and Boogie have made it much easier to build program verifiers, transforming the process into a logic compilation problem rather than a proof automation one. Why3 in particular implements a rich logic for program specification with polymorphism, algebraic data types, recursive functions and predicates, and inductive predicates; it translates this logic to over a dozen solvers and proof assistants. Accordingly, it serves as a backend for many tools, including Frama-C, EasyCrypt, and GNATProve for Ada SPARK. But how can we be sure that these tools are correct? The alternate foundational approach, taken by tools like VST and CakeML, provides strong guarantees by implementing the entire toolchain in a proof assistant, but these tools are harder to build and cannot directly take advantage of SMT solver automation. As a first step toward enabling automated tools with similar foundational guarantees, we give a formal semantics in Coq for the logic fragment of Why3. We show that our semantics are useful by giving a correct-by-construction natural deduction proof system for this logic, using this proof system to verify parts of Why3’s standard library, and proving sound two of Why3’s transformations used to convert terms and formulas into the simpler logics supported by the backend solvers. 

   more » « less
3. Practical Machine-Checked Formalization of Change Impact Analysis

   https://doi.org/10.1007/978-3-030-45237-7_9  

   Palmskog, Karl; Celik, Ahmet; Gligoric, Milos (April 2020, International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

   null (Ed.)
4. Hypothesis Formalization: Empirical Findings, Software Limitations, and Design Implications

   https://doi.org/10.1145/3476980  

   Jun, Eunice; Birchfield, Melissa; De Moura, Nicole; Heer, Jeffrey; Just, René (February 2022, ACM Transactions on Computer-Human Interaction)

   Data analysis requires translating higher level questions and hypotheses into computable statistical models. We present a mixed-methods study aimed at identifying the steps, considerations, and challenges involved in operationalizing hypotheses into statistical models, a process we refer to as hypothesis formalization . In a formative content analysis of 50 research papers, we find that researchers highlight decomposing a hypothesis into sub-hypotheses, selecting proxy variables, and formulating statistical models based on data collection design as key steps. In a lab study, we find that analysts fixated on implementation and shaped their analyses to fit familiar approaches, even if sub-optimal. In an analysis of software tools, we find that tools provide inconsistent, low-level abstractions that may limit the statistical models analysts use to formalize hypotheses. Based on these observations, we characterize hypothesis formalization as a dual-search process balancing conceptual and statistical considerations constrained by data and computation and discuss implications for future tools. 

   more » « less
5. Categorical Databases for Mathematical Formalization of AC Optimal Power Flow

   https://doi.org/10.1109/TPEC56611.2023.10078526  

   Barati, Masoud (February 2023, IEEE)

   It has been decades since category theory was applied to databases. In spite of their mathematical elegance, categorical models have traditionally had difficulty representing factual data, such as integers or strings. This paper proposes a categorical dataset for power system computational models, which is used for AC Optimal Power Flows (ACOPF). In addition, categorical databases incorporate factual data using multi-sorted algebraic theories (also known as Lawvere theories) based on the set-valued functor model. In the advanced metering infrastructure of power systems, this approach is capable of handling missing information efficiently. This methodology enables constraints and queries to employ operations on data, such as multiplicative and comparative processes, thereby facilitating the integration between conventional databases and programming languages like Julia and Python’s Pypower. The demonstration illustrates how all elements of the model, including schemas, instances, and functors, can modify the schema in ACOPF instances. 

   more » « less