Skip to main content

Questions tagged [programming-languages]

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

Filter by
Sorted by
Tagged with
2 votes
1 answer

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 ...
Ashmit's user avatar
  • 21
4 votes
4 answers

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 ...
Kid A's user avatar
  • 43
1 vote
1 answer

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 ...
Daniel Donnelly's user avatar
2 votes
0 answers

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 ...
user2361'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
3 votes
1 answer

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 ...
Daniel Donnelly's user avatar
0 votes
1 answer

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 ...
Daniel Donnelly's user avatar
1 vote
1 answer

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 ...
Daniel Donnelly's user avatar
6 votes
2 answers

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 ...
nicolas's user avatar
  • 193
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
15 votes
2 answers

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 ...
Cheery's user avatar
  • 721