-
Learning Structure-Aware Representations of Dependent Types
Authors:
Konstantinos Kogkalidis,
Orestis Melkonian,
Jean-Philippe Bernardy
Abstract:
Agda is a dependently-typed programming language and a proof assistant, pivotal in proof formalization and programming language theory. This paper extends the Agda ecosystem into machine learning territory, and, vice versa, makes Agda-related resources available to machine learning practitioners. We introduce and release a novel dataset of Agda program-proofs that is elaborate and extensive enough…
▽ More
Agda is a dependently-typed programming language and a proof assistant, pivotal in proof formalization and programming language theory. This paper extends the Agda ecosystem into machine learning territory, and, vice versa, makes Agda-related resources available to machine learning practitioners. We introduce and release a novel dataset of Agda program-proofs that is elaborate and extensive enough to support various machine learning applications -- the first of its kind. Leveraging the dataset's ultra-high resolution, detailing proof states at the sub-type level, we propose a novel neural architecture targeted at faithfully representing dependently-typed programs on the basis of structural rather than nominal principles. We instantiate and evaluate our architecture in a premise selection setup, where it achieves strong initial results.
△ Less
Submitted 3 February, 2024;
originally announced February 2024.
-
Reconciling Event Structures with Modern Multiprocessors
Authors:
Evgenii Moiseenko,
Anton Podkopaev,
Ori Lahav,
Orestis Melkonian,
Viktor Vafeiadis
Abstract:
Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous "out-of-thin-air" problem. Although it has been shown to have important benefits over other memory models, its established compilation schemes are suboptimal in that they add more fences than necessary. In this paper, we prove the correctness in Coq of the intended compilation schemes for W…
▽ More
Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous "out-of-thin-air" problem. Although it has been shown to have important benefits over other memory models, its established compilation schemes are suboptimal in that they add more fences than necessary. In this paper, we prove the correctness in Coq of the intended compilation schemes for Weakestmo to a range of hardware memory models (x86, POWER, ARMv7, ARMv8, RISC-V). Our proof is the first that establishes correctness of compilation of an event-structure-based model that forbids "thin-air" behaviors, as well as the first mechanized compilation proof of a weak memory model supporting sequentially consistent accesses to such a range of hardware platforms. Our compilation proof goes via the recent Intermediate Memory Model (IMM), which we suitably extend with sequentially consistent accesses.
△ Less
Submitted 28 May, 2020; v1 submitted 15 November, 2019;
originally announced November 2019.
-
Having Fun in Learning Formal Specifications
Authors:
I. S. W. B. Prasetya,
Craig Q. H. D. Leek,
Orestis Melkonian,
Joris ten Tusscher,
Jan van Bergen,
J. M. Everink,
Thomas van der Klis,
Petar Kostic,
Rick Meijerink,
Roan Oosenbrug,
Jelle J. Oostveen,
Tijmen van den Pol,
Mike de Vries,
Wink M. van Zon
Abstract:
There are many benefits in providing formal specifications for our software. However, teaching students to do this is not always easy as courses on formal methods are often experienced as dry by students. This paper presents a game called FormalZ that teachers can use to introduce some variation in their class. Students can have some fun in playing the game and, while doing so, also learn the basi…
▽ More
There are many benefits in providing formal specifications for our software. However, teaching students to do this is not always easy as courses on formal methods are often experienced as dry by students. This paper presents a game called FormalZ that teachers can use to introduce some variation in their class. Students can have some fun in playing the game and, while doing so, also learn the basics of writing formal specifications in the form of pre- and post-conditions. Unlike existing software engineering themed education games such as Pex and Code Defenders, FormalZ takes the deep gamification approach where playing gets a more central role in order to generate more engagement. This short paper presents our work in progress: the first implementation of FormalZ along with the result of a preliminary users' evaluation. This implementation is functionally complete and tested, but the polishing of its user interface is still future work.
△ Less
Submitted 1 March, 2019;
originally announced March 2019.
