Groups
Groups
Sign in
Groups
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
Group path
ats-lang-users
Contact owners and managers
1–8 of 1360
Welcome to the ats-lang-users group!
Mark all as read
Report group
0 selected
gmhwxi
,
Artyom Shalkhakov
3
1/6/16
Q&A
Two styles of theorem-proving
I would think so. Z3 is quite advanced. On Wednesday, January 6, 2016 at 12:36:13 AM UTC-5, Artyom
unread,
theorem-proving
Q&A
Two styles of theorem-proving
I would think so. Z3 is quite advanced. On Wednesday, January 6, 2016 at 12:36:13 AM UTC-5, Artyom
1/6/16
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
Shea Levy
,
gmhwxi
5
12/3/15
Q&A
Separate declaration and definition of prfn does not respect termination requirements
In ATS1, there is some form of checking that can be enforced to prevent 'primplement' from
unread,
theorem-proving
Q&A
Separate declaration and definition of prfn does not respect termination requirements
In ATS1, there is some form of checking that can be enforced to prevent 'primplement' from
12/3/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
Kiwamu Okabe
, …
gmhwxi
43
6/18/15
How to shape palindrome on ATS/LF?
Congratulations! You finally made it out of the woods :) On Thursday, June 18, 2015 at 1:00:16 PM UTC
unread,
example
theorem-proving
How to shape palindrome on ATS/LF?
Congratulations! You finally made it out of the woods :) On Thursday, June 18, 2015 at 1:00:16 PM UTC
6/18/15
