Programozási nyelv formális szemantikájának kiegészítése lebegőpontos számok ábrázolásával

Témavezető: Lukács Dániel
ELTE Informatikai Kar
email: dlukacs@inf.elte.hu

Projekt leírás

Programozási nyelvek formális szemantikája alatt egy olyan szabályrendszert értünk, mely matematikailag jól definiált leírást ad a nyelv működéséről, amely feldolgozható interaktív tételbizonyító rendszerekkel, és így felhasználható programok tulajdonságainak bizonyítására.

A feladat tárgya egy, az Erlang programozási nyelvet modellező formális szemantika kibővítése lebegőpontos számokkal a Rocq (korábbi nevén Coq) tételbizonyító rendszerben.

A feladat része a lebegőpontos számok szabványainak és a hivatalos Erlang interpreterben való implementációjának tanulmányozása; a jelenlegi Erlang formális szemantika megértése; a lebegőpontos számok típusának, műveleteinek, és kivételes eseteinek modellezése a szemantikában.

A cél egy olyan modell kialakítása, amely az Erlang interpreterben szereplő ábrázolással azonosan működik, és amelynek helyességére vonatkozóan alapvető tételek is bizonyíthatóak.

A feladatvégzés során a hallgatók megismerkednek az Erlang nyelvvel, a Rocq tételbizonyító rendszerrel, valamint a magasszintű programozási nyelvek modellezésének kérdéseivel.

Előfeltételek

A feladathoz tetszőleges funkcionális programozási nyelv (pl. Erlang, Clojure, Lisp, Mathematica, Haskell, OCaml) ismerete, valamint alapos matematikai logikai és bizonyításelméleti ismeretek és készségek megléte ajánlott.

Hivatkozások

  1. Péter Bereczky, Dániel Horpácsi, and Simon Thompson. 2024. A frame stack semantics for sequential Core Erlang. In Proceedings of the 35th Symposium on Implementation and Application of Functional Languages. ACM, New York, NY, USA, 13 pages. doi:10.1145/3652561.3652566. URL: https://dl.acm.org/doi/10.1145/3652561.3652566
  2. High-Assurance Refactoring Project. 2026. Core Erlang formalization. URL: https://github.com/harp-project/Core-Erlang-Formalization
  3. Ericsson AB. “Representation of Floating-Point Numbers”. Erlang System Documentation. 2026. URL: https://www.erlang.org/doc/system/data_types.html#representation-of-floating-point-numbers
  4. Inria 2025. The Rocq proof assistant. URL: https://rocq-prover.org