ATS looks very interesting and no, I havne't seen this before.
I will look into it.
Axiom will be implemented in Common Lisp for a lot of reasons,
not the least of which is that it depends on certain Lisp features
to implement some algorithms.
That said, I'm studying and implememting ideas from o
If you have looked at ATS lang and rejected it for your purpose
then just ignore rest of mail.
ATS programming language (http://www.ats-lang.org/)
For more information (https://github.com/githwxi/ATS-Postiats/wiki)
I think ATS is worth a look at least once if you are looking for
lang/system that
Of particular interest is clarity.
I've been working with LEAN. The code is in C++ and is very
clever. For instance, there is a beautiful macro embedded in
data structures to perform reference counting.
Unfortunately, I can't reverse-engineer the logic rules that are
embedded in the C++ code.
HO
Tim,
I can see how you can prove individual algorithms correct and I can see
how you can use a proven Lisp but, if you want to prove "down to the
metal", it looks to me like there is an enormous gap in-between which is
SPAD.
Can you really prove SPAD correct?
You mention a specification lan
Hmm. The problem to be solved involves several parts.
Idris is of interest in PART 6, 7, and 8 below.
PART 1: We have the domain
We have GCD in NAT (axiom: NonNegativeInteger or NNI)
NonNegativeInteger is what Axiom calls a "Domain", which means
that it contains signatures, such as
quo : (%,%
On 21/09/2019 13:40, Henri Tuhola wrote:
The elaborator reflection also allows accessing the term rewriting. I
suppose that's all you need in order to write a program that
simplifies equations inside the type context?
I am trying to understand if these equations could be solved in this way?
I
Idris has a way to present equalities like this:
addition_unit : (a:Nat) -> (a + 0) = a
addition_s : (a,b:Nat) -> (a + S b) = S (a + b)
add_commutative : (a,b:Nat) -> (a + b = b + a)
They can be used to prove more things:
try_out : (x,y:Nat) -> ((x + 0) + y) = y + x
try_out x y = rewrite additio
I'm a fan of both Axiom and Idris. I think my ideal would be Axiom
mathematics build on top of the Idris type system.
The Axiom type system was incredibly advanced for its time but I suspect
the Idris type system has finally caught up and overtaken it? Correct me
if I'm wrong but I think the A
Axiom has type information everywhere. It is strongly
dependently typed. So give a Polynomial type, which
Axiom has, over a Ring or Field, such as
Polynomial(Integer) or Polynomial(Fraction(Integer))
we can use theorems from the Ring while proving
properties of Polynomials.
Axiom has a deep type h
I doubt it does cover that. And I think there would be at least two
approaches to implement GCD for polynomials in Idris.
Obvious approach would be to construct a type that represents
polynomials on some base number and variables. For example,
(Polynomial Nat [X]). You would then prove GCD for thi
Does the Idris code cover GCD for polynomials?
On 9/20/19, Henri Tuhola wrote:
> You can already define and prove gcd in idris/agda/coq. It's not too hard
> either.
>
> This weekend I am trying to prove transitive closure can be computed in
> Idris. The way I represent it is that I have f:(a ->
You can already define and prove gcd in idris/agda/coq. It's not too hard
either.
This weekend I am trying to prove transitive closure can be computed in
Idris. The way I represent it is that I have f:(a -> a -> Type), this forms
a type that is inhabited when a statement is true. I can wrap this i
https://www.youtube.com/watch?v=uLCqJLFP7f8
The above link is about SEL4, the proven kernel.
They have about 1 million lines of proof.
I've been looking at the issue of "proof down to the metal".
It seems that SEL4 will run on an ARM processor which
is the basis for the Raspberry PI. I have a PI
13 matches
Mail list logo
