Groups
Sign in
Groups
ats-lang-users
Conversations
Labels
API
ATS3
AVR
Clojure
Erlang
IDE
JVM
JavaScript
PHP
Perl
Python
Scheme
arduino
atsccomp
build
call-by-reference
call-by-value
closure
constraint
contribute
datatype
dependent-type
documentation
effect
emacs
example
general
high-order
install
library
license
linear-closure
linear-type
macro
package
polymorphism
portability
proof
refinement
session
stack-allocation
stream
syntax
tail-recursion
template
termination
theorem-proving
tutorial
type
type-error
About
Send feedback
Help
ats-lang-users
Contact owners and managers
1–15 of 1347
Welcome to the ats-lang-users group!
Mark all as read
Report group
0 selected
Yannick Duchêne
,
Hongwei Xi
9
8/4/18
Q&A
Effects of proofs on types as a side effect
Le samedi 4 août 2018 16:43:28 UTC+2, gmhwxi a écrit : Here is what I have in mind at this moment:
unread,
proof
type
Q&A
Effects of proofs on types as a side effect
Le samedi 4 août 2018 16:43:28 UTC+2, gmhwxi a écrit : Here is what I have in mind at this moment:
8/4/18
Brandon Barker
, …
Yannick Duchêne
8
3/24/19
Q&A
proofs vs statics?
Yes, indeed, there are proof functions and proof values (as result of proof functions) ; the word “
unread,
proof
Q&A
proofs vs statics?
Yes, indeed, there are proof functions and proof values (as result of proof functions) ; the word “
3/24/19
Yannick Duchêne
,
gmhwxi
6
12/21/15
Q&A
Proof derivation and functional relation (deterministic)
Le lundi 21 décembre 2015 17:17:50 UTC+1, gmhwxi a écrit : I think what you need is to define
unread,
proof
theorem-proving
tutorial
Q&A
Proof derivation and functional relation (deterministic)
Le lundi 21 décembre 2015 17:17:50 UTC+1, gmhwxi a écrit : I think what you need is to define
12/21/15
Yannick Duchêne
,
Hongwei Xi
3
12/18/15
Q&A
Proof values: is there an equality/inequality operator?
So it has to be user defined. In a way, that make sense too, as proof values can be made up of
unread,
proof
theorem-proving
Q&A
Proof values: is there an equality/inequality operator?
So it has to be user defined. In a way, that make sense too, as proof values can be made up of
12/18/15
gmhwxi
12/15/15
Q&A
Encoding propositional logic
I turned some of my lecture notes into an article in the Effective-ATS series: http://ats-lang.
unread,
proof
theorem-proving
Q&A
Encoding propositional logic
I turned some of my lecture notes into an article in the Effective-ATS series: http://ats-lang.
12/15/15
Yannick Duchêne
,
gmhwxi
21
12/13/15
Q&A
Stadef and stacst questions: am I missing Skolen constants?
Le dimanche 13 décembre 2015 22:21:11 UTC+1, gmhwxi a écrit : From Q to P: prfn Q2P (pf: Q): P = let
unread,
constraint
proof
theorem-proving
Q&A
Stadef and stacst questions: am I missing Skolen constants?
Le dimanche 13 décembre 2015 22:21:11 UTC+1, gmhwxi a écrit : From Q to P: prfn Q2P (pf: Q): P = let
12/13/15
Yannick Duchêne
,
gmhwxi
6
12/12/15
Q&A
`dataprop`: is requiring multiple premisses instead of a single one possible?
I would suggest that you declare DATA as an abstract prop. Instead of introducing constructors like
unread,
example
proof
syntax
Q&A
`dataprop`: is requiring multiple premisses instead of a single one possible?
I would suggest that you declare DATA as an abstract prop. Instead of introducing constructors like
12/12/15
gmhwxi
, …
john skaller
13
6/16/15
Q&A
Quantifed constraints
On 17/06/2015, at 7:26 AM, H Zhang wrote: > You might want to try Kodkod http://alloy.mit.edu/
unread,
constraint
proof
theorem-proving
Q&A
Quantifed constraints
On 17/06/2015, at 7:26 AM, H Zhang wrote: > You might want to try Kodkod http://alloy.mit.edu/
6/16/15
Yannick Duchêne
,
Hongwei Xi
2
5/23/15
Q&A
What is the `>>` operator?
Yes, your guess is correct. >>then why not returning a new proof instead This is called proof
unread,
documentation
proof
Q&A
What is the `>>` operator?
Yes, your guess is correct. >>then why not returning a new proof instead This is called proof
5/23/15
Koji Hattori
, …
Yannick Duchêne
6
5/22/15
Q&A
Proofs affecting the dynamic semantics?
It's there: https://www.cs.bu.edu/~hwxi/academic/papers/types07.pdf Got it from here: https://www
unread,
proof
Q&A
Proofs affecting the dynamic semantics?
It's there: https://www.cs.bu.edu/~hwxi/academic/papers/types07.pdf Got it from here: https://www
5/22/15
Yannick Duchêne
,
gmhwxi
9
5/14/15
Q&A
Assumptions generated from case statements?
You could also write: If cond1 * cond2 then ... Note that '*' is a function; both cond1 and
unread,
proof
Q&A
Assumptions generated from case statements?
You could also write: If cond1 * cond2 then ... Note that '*' is a function; both cond1 and
5/14/15
Yannick Duchêne
,
gmhwxi
5
4/12/15
Q&A
Can static variables play the role of ghost variables (as in SPARK‑Ada)?
Here is my understanding of the situation: You have two functions foo1 and foo2. And you want to
unread,
general
proof
Q&A
Can static variables play the role of ghost variables (as in SPARK‑Ada)?
Here is my understanding of the situation: You have two functions foo1 and foo2. And you want to
4/12/15
Yannick Duchêne
, …
Brandon Barker
11
5/19/15
Q&A
What exactly do `prfun` and `prval`?
Le mardi 10 février 2015 02:17:15 UTC+1, Brandon Barker a écrit : On Mon, Feb 9, 2015 at 8:15 PM,
unread,
documentation
proof
Q&A
What exactly do `prfun` and `prval`?
Le mardi 10 février 2015 02:17:15 UTC+1, Brandon Barker a écrit : On Mon, Feb 9, 2015 at 8:15 PM,
5/19/15
Brandon Barker
,
Hongwei Xi
4
2/2/15
Q&A
modulo in constraints
The type for my_mod2 does not look right. On Mon, Feb 2, 2015 at 9:39 PM, Brandon Barker <brandon.
unread,
constraint
dependent-type
proof
Q&A
modulo in constraints
The type for my_mod2 does not look right. On Mon, Feb 2, 2015 at 9:39 PM, Brandon Barker <brandon.
2/2/15
hw...@bu.edu
,
gmhwxi
2
11/6/14
Q&A
prfun, extern and implement
For implementing a proof function, you need to use the keyword primplmnt or primplement On Thursday,
unread,
proof
Q&A
prfun, extern and implement
For implementing a proof function, you need to use the keyword primplmnt or primplement On Thursday,
11/6/14