# Questions tagged [programming-languages]

A formal language (theory) for expressing programs. Used and studied in computer science. (from nLab)

12 questions
Filter by
Sorted by
Tagged with
73 views

### How to find the data type of a Json value that in lean4, to perform type validation. (Functional programming in lean)

Basically I am taking in a json object in lean4 as input and I want to check whether a particular feild like 'age' should always be Nat not something else depending on the schema that the user has ...
• 21
512 views

### Proof Assistants in OOP languages

I am new to the subject of proof assistant software, and I am willing to make one later (about some years later) by myself. I have started self-studying HoTT, Logic and Category theory. But through ...
• 43
1 vote
78 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 ...
65 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
413 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
246 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 ...
119 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 ...
119 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 ...
1 vote
484 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 ...
1k 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 ...
• 193
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 ...
• 2,034