Questions tagged [formal-languages]

A formal language is a collection of words over an alphabet, i.e. strings of symbols from the alphabet, according to certain rules. (from nLab)

Filter by
Sorted by
Tagged with
0 votes
0 answers

Formalization of partial functions for combinatorial counting

I need assistance in defining axioms for partial functions in total function theory that is available in Coq. Specifically, I'm looking for a constructive definition of a partial function that ...
arshiamoeini's user avatar
0 votes
1 answer

Can context-free languages be automatically formalized with Metamath?

In this introduction to Metamath, the author suggests that the $c and $v statements can be viewed as encoding the terminals and ...
Corbin's user avatar
  • 119
2 votes
0 answers

Formally verified email or communication?

This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway. I would like to consider the simplest possible formally verified ...
Julius Hamilton's user avatar
3 votes
2 answers

Are there minimal typed proof verifiers that can deal with the majority of mathematics?

I would like to know if there are proof verifiers that can deal with the majority of mathematics (definitions, theorems, proofs with verification), while also having a minimal implementation. I am not ...
Lewwwer's user avatar
  • 131
4 votes
1 answer

How can you represent a dependent type visually?

So, obviously for a term $t$ of type $T$, I would represent it as: T +-----------+ | | | t | | | +-----------+ That is a node ...
Daniel Donnelly's user avatar
1 vote
1 answer

Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?

I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app ...
Daniel Donnelly's user avatar
19 votes
3 answers

Can the language of proof assistants be used for general purpose programming?

Planning on learning lean/lean4, I was wondering if a proof assistant system like lean4 can be used for general purpose programming? For example, can it replace a language like Standard ML? More ...
tinlyx's user avatar
  • 2,034