k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] Twelf

From: Suminda Dharmasena <sirinath AT sakrio.com>
To: "Rosu, Grigore" <grosu AT illinois.edu>
Cc: "info AT kframework.org" <info AT kframework.org>, "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: Re: [K-user] Twelf
Date: Thu, 2 Jan 2014 11:41:55 +0530
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

Yes.

And also all the infrastructure around the language should be generated from the definition. Also some higher level abstraction of the K syntax it self for reuse and make common usage easy and provide more sugar.

One issue is that since K is in Java means that K is not verified.

Also perhaps K can get its own prover and eliminate the use of Maude and GPL code.

Also a ability to generate a super compiler and tools through constraints from 1 format definition to another would be great.

Re: [K-user] Twelf, Suminda Dharmasena, 01/01/2014
- Re: [K-user] Twelf, Rosu, Grigore, 01/01/2014
  - Re: [K-user] Twelf, Suminda Dharmasena, 01/02/2014