Questions tagged [programming-languages]
A formal language (theory) for expressing programs. Used and studied in computer science. (from nLab)
10
questions
1
vote
1
answer
70
views
Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?
The data I'm referring to is just an easy to understand JSON format of objects / arrows and the styling information about the arrows.
For example, if an arrow is two-headed I need in Coq locally to ...
- 269
2
votes
0
answers
52
views
Tool for typing mathematical physics, e.g. differential geometry
Many expressions in mathematical physics use a rather sloppy notation, e.g. the Lie bracket on a vector field is defined using ambiguous notation, where $X : M \rightarrow TM$ is first defined as a ...
- 21
3
votes
2
answers
355
views
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 ...
- 131
4
votes
1
answer
235
views
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 ...
- 269
3
votes
1
answer
109
views
Do implementations of a PA and of ATP have overlap?
I'm wondering how much overlap (read: code-reusage) there is between a PA and an ATP system.
Are they based upon the same type system at least?
I'm wondering, because right now I'm working on ...
- 269
0
votes
1
answer
103
views
How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?
Here is a link to the "Pierce Book" or Benjamin Pierce's draft transcript of (the first part of) "Types and Programming Languages".
On PDF page 28 you'll see an OCaml ...
- 269
1
vote
1
answer
325
views
How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?
Question:
Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms.
I'm wondering whether Lean4 (or a typical well-known PA) just ...
- 269
5
votes
2
answers
995
views
Using proof assistants to generate fast code
Proof assistants allow to state that
$$A(BC) = (AB)C$$
with $A$,$B$,$C$ compatible matrices,
Is there a formal system that takes this sort of equations to choose among interpretation strategies of ...
- 183
16
votes
3
answers
7k
views
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 ...
- 1,700
15
votes
2
answers
197
views
Can theorem provers be used to form foundations for programming languages?
I started programming a Haskell-clone recently (source code).
After basic hindley-milner, problems start to arise. Implementation of data/codata statements seem to ensure my language is breaking up on ...
- 681