Реализация языкового сервера для интерактивного доказателя теорем Rzk

Implementing a Language Server for the Rzk Proof Assistant

Article's language
English
Author(s)
Abdelrahman Abounegm
Nikolai Dmitrievich Kudasov
Abstract
This paper presents the work in progress implementation of the language server for the Rzk proof assistant. It analyzes relevant technologies related to Language Server Protocol, VS Code extensions, and theorem provers, and builds on top of them for Rzk’s language support.
Keywords
Language Server Protocol
Visual Studio Code extension
proof assistant
homotopy type theory
category theory
DOI
10.31144/si.2307-6410.2023.n22.p45-50
UDK
004.4’232
Pages
45-50
File
abounegmkudasov2023_0.pdf485.63 KB
Number
# 22, 2023