ats-lang-users Mailing List for The ATS PL System
Unleashing the potentials of types and templates
Status: Beta
Brought to you by:
ats-hwxi
You can subscribe to this list here.
2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
(2) |
Aug
(1) |
Sep
(18) |
Oct
(20) |
Nov
(13) |
Dec
(6) |
---|---|---|---|---|---|---|---|---|---|---|---|---|
2009 |
Jan
(51) |
Feb
(10) |
Mar
(1) |
Apr
(13) |
May
(11) |
Jun
(7) |
Jul
(14) |
Aug
|
Sep
(6) |
Oct
(18) |
Nov
(24) |
Dec
(18) |
2010 |
Jan
(4) |
Feb
(19) |
Mar
(8) |
Apr
(34) |
May
(27) |
Jun
(28) |
Jul
(12) |
Aug
(82) |
Sep
(21) |
Oct
(56) |
Nov
(41) |
Dec
(27) |
2011 |
Jan
(32) |
Feb
(34) |
Mar
(12) |
Apr
(102) |
May
(31) |
Jun
(12) |
Jul
(14) |
Aug
(17) |
Sep
(113) |
Oct
(46) |
Nov
(16) |
Dec
(61) |
2012 |
Jan
(72) |
Feb
(41) |
Mar
(43) |
Apr
(19) |
May
(9) |
Jun
(16) |
Jul
(27) |
Aug
|
Sep
(41) |
Oct
(3) |
Nov
(38) |
Dec
(47) |
2013 |
Jan
(27) |
Feb
(59) |
Mar
(12) |
Apr
(39) |
May
(34) |
Jun
(62) |
Jul
(17) |
Aug
(8) |
Sep
(36) |
Oct
(3) |
Nov
(12) |
Dec
(19) |
2014 |
Jan
(6) |
Feb
(5) |
Mar
(43) |
Apr
(35) |
May
(32) |
Jun
(1) |
Jul
(15) |
Aug
(61) |
Sep
(7) |
Oct
(60) |
Nov
(16) |
Dec
(18) |
2015 |
Jan
(26) |
Feb
(13) |
Mar
(12) |
Apr
(10) |
May
(17) |
Jun
(29) |
Jul
(18) |
Aug
(11) |
Sep
(4) |
Oct
(26) |
Nov
(13) |
Dec
(1) |
2016 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
(1) |
Jun
(1) |
Jul
(1) |
Aug
|
Sep
(1) |
Oct
(1) |
Nov
(1) |
Dec
(1) |
2017 |
Jan
(2) |
Feb
(5) |
Mar
(1) |
Apr
(3) |
May
(6) |
Jun
(1) |
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
(1) |
Dec
|
2018 |
Jan
(1) |
Feb
(1) |
Mar
(4) |
Apr
|
May
|
Jun
(3) |
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
|
Dec
|
2019 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
(2) |
2020 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
(2) |
Sep
|
Oct
(1) |
Nov
(2) |
Dec
|
2021 |
Jan
(1) |
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
(2) |
2022 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(1) |
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2024 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
(1) |
Oct
|
Nov
|
Dec
|
From: Raoul D. <ra...@gm...> - 2024-09-19 21:44:10
|
the few purported links i've seen are broken for me. |
From: Son H. <T.S...@so...> - 2022-05-18 18:44:31
|
(Apologies if you got multiple copies of this invitation) ---------------------------------------------------------------------------------------------------------------- CfP: F-IDE, 7th Workshop on Formal Integrated Development Environment affiliated with SEFM 2022, September 26, 2022, Berlin, Germany Abstract registration deadline: 24 July 2022 Submission deadline: 31 July 2022 Notification: 23 August 2022 Website: https://sites.google.com/unipi.it/websitef-ide2022/home-page Topics: formal methods, ide, theoretical computer science ---------------------------------------------------------------------------------------------------------------- OVERVIEW High levels of safety, security, and privacy standards require the use of formal methods to specify and develop compliant software (sub-)systems. Any standard comes with an assessment process, which requires a complete application documentation to ease the justification of design choices and the review of code and proofs. Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logic or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process. TOPICS The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis, and documentation. It welcomes the presentation of tools, methods, techniques and experiments. Topics of interest include, but are not limited to, the following: - F-IDE building: design and integration of languages, development of user-friendly front-ends - How to make high-level logical and programming concepts palatable to industrial developers - Integration of Object-Oriented and modularity features - Integration of static analyzers - Integration of automatic proof tools, theorem provers and testing tools - Documentation tools - Impact of tools on certification - Experience reports on developing F-IDEs - Experience reports on using F-IDEs - Experience reports on formal methods-based assessments in industrial applications SUBMISSION GUIDELINES We accept both long (15 pages) and short (6 pages) paper submissions. The page limit does not include the bibliography. Submitted papers must present original contributions whose main results and conclusions have not been published or submitted elsewhere. Each submission will be reviewed by at least three members of the Program Committee. Submitted papers must be written in English and follow the LNCS style format. Authors are invited to submit the following types of contributions: - Research papers providing new concepts and results - Experience reports - Position papers and research perspectives - Tool presentations Papers should be submitted via EasyChair at F-IDE 2022's workshop page. Preliminary proceedings will be made available in electronic form at the workshop. Post-proceedings are planned to be published in Springer's Lecture Notes in Computer Science series. IMPORTANT DATES * Abstract submission: Sunday 24 July 2022 * Paper submission: 31 July 2022 * Notification: 23 August 2022 * Camera-ready version: 13 September 2022 * Workshop date: 26 September 2022 ORGANIZATION Program Committee - Aaron Dutle, NASA LaRC, USA - Andrea Domenici, University of Pisa, Italy - Bernhard Rumpe, RWTH Aachen University, Germany - Carlo A. Furia, Università della Svizzera Italiana, Switzerland - Enrico Tassi, INRIA, France - Franco Mazzanti, ISTI/CNR, Italy - François Pessaux, ENSTA ParisTech, France - José Proença, CISTER/ISEP, Portugal - Laurent Voisin, Systerel, France - Makarius Wenzel, sketis.net, Germany - Marco Feliu, NIA/NASA LaRC, USA - Markus A. Kuppe, Microsoft Research, USA - Mattias Ulbrich, Karlsruhe Institute of Technology, Germany - Rosemary Monahan, Maynooth University, Ireland - Simão Melo de Sousa, University of Beira Interior, Portugal - Stefan Mitsch, Carnegie Mellon University, USA - Stephan Merz, Inria Nancy, France - Virgile Prevosto, Université Paris-Saclay, CEA, List, France - Yannick Moy, AdaCore, France - Yi Zhang, Massachusetts General Hospital, USA PC chairs - Cinzia Bernardeschi, University of Pisa, Italy - Son Hoang, University of Southampton, UK Steering Committee - Catherine Dubois, Samovar, ENSIIE, France - Paolo Masci, US National Institute of Aerospace (NIA), USA - Dominique Méry, LORIA, Université de Lorraine, France ---------------------------------------------------------------------------------------------------------------- All questions about submissions should be emailed to cin...@un...<mailto:cin...@un...>, T.S...@so...<mailto:T.S...@so...>. ---------------------------------------------------------------------------------------------------------------- -- Dr Son Hoang ECS, University of Southampton SO17 1BJ, Southampton UK |
From: Hans V. <keg...@gm...> - 2021-12-04 02:25:41
|
fun oneLoop (ui : &ui >> _) : void = solved it. Thank you Hongwei! On Fri, Dec 3, 2021 at 8:38 PM Hans Vejle <keg...@gm...> wrote: > > Hello Dr. Xi & friends, > > I am a very stupid man when it comes to types, and I'm working on my > first ATS project using SDL and Emscripten. It worked right away, > which felt amazing! However, I'm trying to understand how I can pass > around a var like I do !type to avoid consuming the linear proof and > still be able to mutate the argument. (Perhaps assuming this makes > sense is my mistake.) > > I found a few posts on this list about creating "takeout/putback" > prvals, as well as this excellent post > https://bluishcoder.co.nz/2011/04/25/sharing-linear-resources-in-ats.html > which came very close, but unfortunately I was unable to figure out > how to apply it to my problem of passing around a reference to a var > of a viewtype whose proofs I want to avoid consuming while still being > able to mutate the argument. > > The below compiles if I don't attempt to set any field of ui, but If I > uncomment either the ui.dimensions or ui.running :=, I get an error > that seems to indicate that the l1 proof for ui was consumed. > > 10062(line=333, offs=5) -- 10064(line=333, offs=7): error(3): unsolved > constraint: C3NSTRprop(C3TKmain(); S2Eeqeq(S2Evar(l1$9081(14901)); > S2Evar(l1$9028(14847)))) > src/main.dats: 10062(line=333, offs=5) -- 10064(line=333, offs=7): > error(3): unsolved constraint for var preservation > typechecking has failed: there are some unsolved constraints: please > inspect the above reported error message(s) for information. > > This makes sense to me since I'm passing &ui, not !ui. If I change the > argument of oneLoop to !ui (whether ui is an @ or '), I get this > error: > > 9865(line=324, offs=34): error(3): a non-proof component is replaced > of the type: [S2Ecst(bool)]. > > I assume this is because the argument is no longer mutable. > > Should I not be trying to use a viewtype var this way? > > Thank you in advance, > Hans > > PS: Bonus question: Is there a way in ATS to do the matching of > SDL_Event below as a switch statement (i.e. pattern-matching on > $extval constants)? > > --- > > typedef dimensions = > @{ width = int > , height = int > , refreshRate = int > } > > viewtypedef ui (l1 : addr, l2 : addr, l3 : addr) = > @{ window = SDL_Window l1 > , renderer = SDL_Renderer l2 > , font = TTF_Font l3 > , dimensions = dimensions > , running = bool > } > > viewtypedef ui = [l1, l2, l3 : agz] ui(l1, l2, l3) > > // (SDL_Window/Renderer/TTF_Font are addr absviewtypes + agz > viewtypedef as you'd expect) > > typedef callback = (&ui) -<fun1> void > > extern fun emscripten_set_main_loop_arg (func : callback, arg : &ui, > fps : int, simulate_infinite_loop : bool) : void = "mac#" > > fun oneLoop (ui : &ui) : void = > let > var e : SDL_Event > val () = e.type := $Unsafe.cast 0 > var pollRet : int = SDL_PollEvent e > val () = > while (pollRet = 1) ( > let > val () = > if e.type = SDL_MOUSEMOTION > then () > else if e.type = SDL_WINDOWEVENT > then () // ui.dimensions := getWindowDimensions ui.window > else if e.type = SDL_QUIT > then () // ui.running := false > else () > in > pollRet := SDL_PollEvent e > end > ) > // val () = draw ui > in > () > end > > implement main0 () = > let > ... > var ui : ui (null, null, null) > val () = ui.running := true > val () = ui.dimensions := getDesktopDimensions () > val () = ui.window := SDL_CreateWindow ("risk", 0, 0, > ui.dimensions.width, ui.dimensions.height, > SDL_WINDOW_SHOWN_RESIZABLE_OPENGL_HIGHDPI) > val () = ui.renderer := SDL_CreateRenderer (ui.window, ~1, > SDL_RENDERER_ACCELERATED) > val () = ui.font := TTF_OpenFont ("fonts/UbuntuMono-R.ttf", 64) > val ((* main loop *)) = emscripten_set_main_loop_arg(oneLoop, ui, 0, true) > val () = SDL_DestroyRenderer ui.renderer > val () = SDL_DestroyWindow ui.window > val () = TTF_CloseFont ui.font > val () = TTF_Quit () > val () = SDL_FreeCursor cursorArrow > val () = SDL_Quit () > in > () > end |
From: Hans V. <keg...@gm...> - 2021-12-04 01:38:56
|
Hello Dr. Xi & friends, I am a very stupid man when it comes to types, and I'm working on my first ATS project using SDL and Emscripten. It worked right away, which felt amazing! However, I'm trying to understand how I can pass around a var like I do !type to avoid consuming the linear proof and still be able to mutate the argument. (Perhaps assuming this makes sense is my mistake.) I found a few posts on this list about creating "takeout/putback" prvals, as well as this excellent post https://bluishcoder.co.nz/2011/04/25/sharing-linear-resources-in-ats.html which came very close, but unfortunately I was unable to figure out how to apply it to my problem of passing around a reference to a var of a viewtype whose proofs I want to avoid consuming while still being able to mutate the argument. The below compiles if I don't attempt to set any field of ui, but If I uncomment either the ui.dimensions or ui.running :=, I get an error that seems to indicate that the l1 proof for ui was consumed. 10062(line=333, offs=5) -- 10064(line=333, offs=7): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eeqeq(S2Evar(l1$9081(14901)); S2Evar(l1$9028(14847)))) src/main.dats: 10062(line=333, offs=5) -- 10064(line=333, offs=7): error(3): unsolved constraint for var preservation typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information. This makes sense to me since I'm passing &ui, not !ui. If I change the argument of oneLoop to !ui (whether ui is an @ or '), I get this error: 9865(line=324, offs=34): error(3): a non-proof component is replaced of the type: [S2Ecst(bool)]. I assume this is because the argument is no longer mutable. Should I not be trying to use a viewtype var this way? Thank you in advance, Hans PS: Bonus question: Is there a way in ATS to do the matching of SDL_Event below as a switch statement (i.e. pattern-matching on $extval constants)? --- typedef dimensions = @{ width = int , height = int , refreshRate = int } viewtypedef ui (l1 : addr, l2 : addr, l3 : addr) = @{ window = SDL_Window l1 , renderer = SDL_Renderer l2 , font = TTF_Font l3 , dimensions = dimensions , running = bool } viewtypedef ui = [l1, l2, l3 : agz] ui(l1, l2, l3) // (SDL_Window/Renderer/TTF_Font are addr absviewtypes + agz viewtypedef as you'd expect) typedef callback = (&ui) -<fun1> void extern fun emscripten_set_main_loop_arg (func : callback, arg : &ui, fps : int, simulate_infinite_loop : bool) : void = "mac#" fun oneLoop (ui : &ui) : void = let var e : SDL_Event val () = e.type := $Unsafe.cast 0 var pollRet : int = SDL_PollEvent e val () = while (pollRet = 1) ( let val () = if e.type = SDL_MOUSEMOTION then () else if e.type = SDL_WINDOWEVENT then () // ui.dimensions := getWindowDimensions ui.window else if e.type = SDL_QUIT then () // ui.running := false else () in pollRet := SDL_PollEvent e end ) // val () = draw ui in () end implement main0 () = let ... var ui : ui (null, null, null) val () = ui.running := true val () = ui.dimensions := getDesktopDimensions () val () = ui.window := SDL_CreateWindow ("risk", 0, 0, ui.dimensions.width, ui.dimensions.height, SDL_WINDOW_SHOWN_RESIZABLE_OPENGL_HIGHDPI) val () = ui.renderer := SDL_CreateRenderer (ui.window, ~1, SDL_RENDERER_ACCELERATED) val () = ui.font := TTF_OpenFont ("fonts/UbuntuMono-R.ttf", 64) val ((* main loop *)) = emscripten_set_main_loop_arg(oneLoop, ui, 0, true) val () = SDL_DestroyRenderer ui.renderer val () = SDL_DestroyWindow ui.window val () = TTF_CloseFont ui.font val () = TTF_Quit () val () = SDL_FreeCursor cursorArrow val () = SDL_Quit () in () end |
From: Andrei P. <and...@lr...> - 2021-02-24 20:53:56
|
****************************************************************** F-IDE 2021: 6th Workshop on Formal Integrated Development Environment Affiliated with NASA Formal Methods 2021 May 24-25, 2021 -- held online https://cister-labs.pt/f-ide2021 ****************************************************************** Keynotes * Prof. Jan Friso Groote, Eindhoven Univ. of Technology, the Netherlands * Benoît Rognier, Edukera, France Important Dates * Abstract submission - extended: Mon, Mar 8, 2021 * Full paper submission - extended: Mon, Mar 15, 2021 * Notification: Mon, Apr 19, 2021 * Camera-ready: Mon, May 3, 2021 * Workshop: May 24-25, 2021 Overview High levels of safety, security, and privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application to ease the justification of design choices and the review of code and proofs. Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language and/or an environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process. Topics The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis, and documentation. It welcomes the presentation of tools, methods, techniques, and experiments. Topics of interest include, but are not limited to, the following: * F-IDE building: design and integration of languages, development of user-friendly front-ends * How to make high-level logical and programming concepts palatable to industrial developers * Integration of object-oriented and modularity features * Integration of static analyzers * Integration of automated proof tools, theorem provers, and testing tools * Documentation tools * Impact of tools on certification * Experience reports on developing F-IDEs * Experience reports on using F-IDEs * Experience reports on formal methods-based assessments in industrial applications Submission Guidelines We accept both long (15 pages) and short (6 pages) paper submissions. The page limit does not include the bibliography. Submitted papers must present original contributions whose main results and conclusions have not been published or submitted elsewhere. Each submission will be reviewed by at least three members of the Program Committee. We expect that one author of every accepted paper will present their work at the workshop. Submitted papers must be written in English and follow the EPTCS LaTeX format (http://style.eptcs.org). Authors are invited to submit the following types of contributions: * Research papers providing new concepts and results * Experience reports * Position papers and research perspectives * Tool presentations Papers should be submitted via EasyChair at F-IDE 2021's workshop page: https://easychair.org/conferences/?conf=f-ide2021. Preliminary proceedings will be made available in electronic form at the workshop. Post-proceedings will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Program Committee * Andrew Reynolds, University of Iowa, USA * Damien Doligez, Inria, France * Bernhard Rumpe, RWTH Aachen University, Germany * Carlo A. Furia, Chalmers University of Technology, Sweden * César Muñoz, NASA Langley, USA * Cinzia Bernardeschi, University of Pisa, Italy * Claudio Sacerdoti Coen, University of Bologna, Italy * Enrico Tassi, Inria, France * François Pessaux, ENSTA ParisTech, France * José Creissac Campos, University of Minho, Portugal * Kenneth Lausdahl, Aarhus University, Denmark * Laurent Voisin, Systerel, France * Lucas Wagner, Collins Aerospace, USA * Makarius Wenzel, sketis.net * Markus A. Kuppe, Microsoft Research, USA * Mattias Ulbrich, Karlsruhe Institute of Technology, Germany * Pierre-Yves Strub, LIX, Ãcole Polytechnique, France * Rosemary Monahan, Maynooth University, Ireland * Silvia Lizeth Tapia Tarifa, University of Oslo, Norway * Simão Melo de Sousa, Universidade Beira Interior, Portugal * Stefan Mitsch, Carnegie Mellon University, USA * Stephan Merz, Inria, France * Virgile Prevosto, Institut List, CEA Tech, Université Paris-Saclay, France * Yannick Moy, AdaCore, France * Yi Zhang, Massachusetts General Hospital, USA PC Chairs * Andrei Paskevich, Université Paris-Saclay, France * José Proença, CISTER/ISEP, Portugal Steering Committee * Catherine Dubois, Samovar, ENSIIE, France * Paolo Masci, US National Institute of Aerospace (NIA), USA * Dominique Méry, LORIA, Université de Lorraine, France |
From: Andrei P. <and...@lr...> - 2021-01-08 18:09:10
|
****************************************************************** F-IDE 2021: 6th Workshop on Formal Integrated Development Environment Affiliated with NASA Formal Methods 2021 May 24-25, 2021 -- held online https://cister-labs.pt/f-ide2021 ****************************************************************** Keynotes * Prof. Jan Friso Groote, Eindhoven Univ. of Technology, the Netherlands * Benoît Rognier, Edukera, France Important Dates * Abstract submission: Mon, Feb 22, 2021 * Full paper submission: Mon, Mar 1, 2021 * Notification: Mon, Apr 19, 2021 * Camera-ready: Mon, May 3, 2021 * Workshop: May 24-25, 2021 Overview High levels of safety, security, and privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application to ease the justification of design choices and the review of code and proofs. Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language and/or an environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process. Topics The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis, and documentation. It welcomes the presentation of tools, methods, techniques, and experiments. Topics of interest include, but are not limited to, the following: * F-IDE building: design and integration of languages, development of user-friendly front-ends * How to make high-level logical and programming concepts palatable to industrial developers * Integration of object-oriented and modularity features * Integration of static analyzers * Integration of automated proof tools, theorem provers, and testing tools * Documentation tools * Impact of tools on certification * Experience reports on developing F-IDEs * Experience reports on using F-IDEs * Experience reports on formal methods-based assessments in industrial applications Submission Guidelines We accept both long (15 pages) and short (6 pages) paper submissions. The page limit does not include the bibliography. Submitted papers must present original contributions whose main results and conclusions have not been published or submitted elsewhere. Each submission will be reviewed by at least three members of the Program Committee. We expect that one author of every accepted paper will present their work at the workshop. Submitted papers must be written in English and follow the EPTCS LaTeX format (http://style.eptcs.org). Authors are invited to submit the following types of contributions: * Research papers providing new concepts and results * Experience reports * Position papers and research perspectives * Tool presentations Papers should be submitted via EasyChair at F-IDE 2021's workshop page: https://easychair.org/conferences/?conf=f-ide2021. Preliminary proceedings will be made available in electronic form at the workshop. Post-proceedings will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Program Committee * Andrew Reynolds, University of Iowa, USA * Damien Doligez, Inria, France * Bernhard Rumpe, RWTH Aachen University, Germany * Carlo A. Furia, Chalmers University of Technology, Sweden * César Muñoz, NASA Langley, USA * Cinzia Bernardeschi, University of Pisa, Italy * Claudio Sacerdoti Coen, University of Bologna, Italy * Enrico Tassi, Inria, France * François Pessaux, ENSTA ParisTech, France * José Creissac Campos, University of Minho, Portugal * Kenneth Lausdahl, Aarhus University, Denmark * Laurent Voisin, Systerel, France * Lucas Wagner, Collins Aerospace, USA * Makarius Wenzel, sketis.net * Markus A. Kuppe, Microsoft Research, USA * Mattias Ulbrich, Karlsruhe Institute of Technology, Germany * Pierre-Yves Strub, LIX, Ãcole Polytechnique, France * Rosemary Monahan, Maynooth University, Ireland * Silvia Lizeth Tapia Tarifa, University of Oslo, Norway * Simão Melo de Sousa, Universidade Beira Interior, Portugal * Stefan Mitsch, Carnegie Mellon University, USA * Stephan Merz, Inria, France * Virgile Prevosto, Institut List, CEA Tech, Université Paris-Saclay, France * Yannick Moy, AdaCore, France * Yi Zhang, Massachusetts General Hospital, USA PC Chairs * Andrei Paskevich, Université Paris-Saclay, France * José Proença, CISTER/ISEP, Portugal Steering Committee * Catherine Dubois, Samovar, ENSIIE, France * Paolo Masci, US National Institute of Aerospace (NIA), USA * Dominique Méry, LORIA, Université de Lorraine, France |
From: Hongwei Xi <hw...@bu...> - 2020-11-14 04:36:05
|
Hi, It is my pleasure to announce the release of ATS2-0.4.2. Note that this is the version currently needed for compiling the ongoing implementation of ATS3 (ATS/Xanadu). ------------------------------------------------ ATS-Postiats-0.4.2.tgz: The same as ATS-Postiats-int-0.4.2.tgz MD5: 900c43b69f544ddff738ebf864f98b06 SHA1: 76b7c817c3439858e42c4ff74edc226578e0ea1b -- ATS2-Postiats-gmp-0.4.2.tgz: MD5: e2f0f6c38868bb6b85f77fd1d9222b23 SHA1: a869ba92d673082cd30fc6c2368d3948eef772fa -- ATS2-Postiats-int-0.4.2.tgz: MD5: 900c43b69f544ddff738ebf864f98b06 SHA1: 76b7c817c3439858e42c4ff74edc226578e0ea1b ------------------------------------------------ This is the 53rd release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ Here is a list of major additions and changes since the last release: There are only a few minor modifications, which are primarily needed for compiling the current (2020-11-01) implementation of ATS3. 1. Fixing the handling of an issue causing the compiler crash: the proof of the at-view of a local variable is not restored at the end of its scope. Please visit the following link for more details: https://groups.google.com/g/ats-lang-users/c/f9QVilhHMEM 2. Fixing bug-2020-10-14 (for the omission of handling records when the exhaustiveness of pattern matching is tested) Kudos to Alex Dambaev for reporting it! Please note that in this release, there are two variants of the package released: The "gmp" variant depends on the GMP library and the "int" variant does not depend on the GMP library. In this release ATS2-Postiats-0.4.2.tgz is just the same as ATS2-Postiats-int-0.4.2.tgz. ###### Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) |
From: Hongwei Xi <hw...@bu...> - 2020-11-14 04:34:39
|
Hi, It is my pleasure to announce the release of ATS2-0.4.2. Note that this is the version currently needed for compiling the ongoing implementation of ATS3 (ATS/Xanadu). ------------------------------------------------ ATS-Postiats-0.4.2.tgz: The same as ATS-Postiats-int-0.4.2.tgz MD5: 900c43b69f544ddff738ebf864f98b06 SHA1: 76b7c817c3439858e42c4ff74edc226578e0ea1b -- ATS2-Postiats-gmp-1.4.0.tgz: MD5: e2f0f6c38868bb6b85f77fd1d9222b23 SHA1: a869ba92d673082cd30fc6c2368d3948eef772fa -- ATS2-Postiats-int-1.4.0.tgz: MD5: 900c43b69f544ddff738ebf864f98b06 SHA1: 76b7c817c3439858e42c4ff74edc226578e0ea1b ------------------------------------------------ This is the 53rd release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ Here is a list of major additions and changes since the last release: There are only a few minor modifications, which are primarily needed for compiling the current (2020-11-01) implementation of ATS3. 1. Fixing the handling of an issue causing the compiler crash: the proof of the at-view of a local variable is not restored at the end of its scope. Please visit the following link for more details: https://groups.google.com/g/ats-lang-users/c/f9QVilhHMEM 2. Fixing bug-2020-10-14 (for the omission of handling records when the exhaustiveness of pattern matching is tested) Kudos to Alex Dambaev for reporting it! Please note that in this release, there are two variants of the package released: The "gmp" variant depends on the GMP library and the "int" variant does not depend on the GMP library. In this release ATS2-Postiats-0.4.2.tgz is just the same as ATS2-Postiats-int-0.4.2.tgz. ###### Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) |
From: Andrei P. <and...@lr...> - 2020-10-19 16:34:21
|
****************************************************************** F-IDE 2021: 6th Workshop on Formal Integrated Development Environment Affiliated with NASA Formal Methods 2021 May 24-28, 2021 -- held online https://cister-labs.pt/f-ide2021 ****************************************************************** Important Dates * Abstract submission: Mon, Feb 22, 2021 * Full paper submission: Mon, Mar 1, 2021 * Notification: Mon, Apr 19, 2021 * Camera-ready: Mon, May 3, 2021 * Workshop: May 24-28, 2021 Overview High levels of safety, security, and privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application to ease the justification of design choices and the review of code and proofs. Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language and/or an environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process. Topics The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis, and documentation. It welcomes the presentation of tools, methods, techniques, and experiments. Topics of interest include, but are not limited to, the following: * F-IDE building: design and integration of languages, development of user-friendly front-ends * How to make high-level logical and programming concepts palatable to industrial developers * Integration of object-oriented and modularity features * Integration of static analyzers * Integration of automated proof tools, theorem provers, and testing tools * Documentation tools * Impact of tools on certification * Experience reports on developing F-IDEs * Experience reports on using F-IDEs * Experience reports on formal methods-based assessments in industrial applications Submission Guidelines We accept both long (15 pages) and short (6 pages) paper submissions. The page limit does not include the bibliography. Submitted papers must present original contributions whose main results and conclusions have not been published or submitted elsewhere. Each submission will be reviewed by at least three members of the Program Committee. We expect that one author of every accepted paper will present their work at the workshop. Submitted papers must be written in English and follow the EPTCS LaTeX format (http://style.eptcs.org). Authors are invited to submit the following types of contributions: * Research papers providing new concepts and results * Experience reports * Position papers and research perspectives * Tool presentations Papers should be submitted via EasyChair at F-IDE 2021's workshop page: https://easychair.org/conferences/?conf=f-ide2021. Preliminary proceedings will be made available in electronic form at the workshop. Post-proceedings will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Program Committee * Andrew Reynolds, University of Iowa, USA * Bernhard Rumpe, RWTH Aachen University, Germany * Carlo A. Furia, Chalmers University of Technology, Sweden * César Muñoz, NASA Langley, USA * Cinzia Bernardeschi, University of Pisa, Italy * Claudio Sacerdoti Coen, University of Bologna, Italy * Enrico Tassi, Inria, France * François Pessaux, ENSTA ParisTech, France * José Creissac Campos, University of Minho, Portugal * Kenneth Lausdahl, Aarhus University, Denmark * Laurent Voisin, Systerel, France * Lucas Wagner, Collins Aerospace, USA * Makarius Wenzel, sketis.net * Markus A. Kuppe, Microsoft Research, USA * Mattias Ulbrich, Karlsruhe Institute of Technology, Germany * Pierre-Yves Strub, LIX, Ãcole Polytechnique, France * Rosemary Monahan, Maynooth University, Ireland * Silvia Lizeth Tapia Tarifa, University of Oslo, Norway * Simão Melo de Sousa, Universidade Beira Interior, Portugal * Stefan Mitsch, Carnegie Mellon University, USA * Stephan Merz, Inria, France * Virgile Prevosto, Institut List, CEA Tech, Université Paris-Saclay, France * Yannick Moy, AdaCore, France * Yi Zhang, Massachusetts General Hospital, USA PC Chairs * Andrei Paskevich, Université Paris-Saclay, France * José Proença, CISTER/ISEP, Portugal Steering Committee * Catherine Dubois, Samovar, ENSIIE, France * Paolo Masci, US National Institute of Aerospace (NIA), USA * Dominique Méry, LORIA, Université de Lorraine, France |
From: Hongwei Xi <hw...@bu...> - 2020-08-03 04:23:03
|
Hi, It is my pleasure to announce the release of ATS2-0.4.1. Note that this is the version needed (or may be needed in the future) for compiling the ongoing implementation of ATS3 (ATS/Xanadu). ------------------------------------------------ ATS-Postiats-0.4.1.tgz: The same as ATS-Postiats-int-0.4.1.tgz MD5: 99d99ea8296035abc7983fc3c21e1f05 SHA1: 1e1d2b33b2f89ca229689de6fc6b403d0d35b6fe -- ATS2-Postiats-gmp-1.4.0.tgz: MD5: 1f73c15ec2fcf0b6880f7a2b3d5da17c SHA1: af6a943b49236f02fcc1fe671477dbff85197c6a -- ATS2-Postiats-int-1.4.0.tgz: MD5: 6bbdd92aa412dd7f70a9e56363b8b22f SHA1: 6c9e4032514a297365ad1f92a17dd61ead70755f ------------------------------------------------ This is the 52nd release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ ###### Here is a list of major additions and changes since the last release: There are only a few minor modifications made to the last release; however, these modifications are needed for compiling ATS3 in the future. ###### Please note that there are two variants of the ATS2 package being released: The "gmp" variant depends on the GMP library and the "int" variant does not depend on the GMP library. In this release ATS2-Postiats-0.4.1.tgz is just the same as ATS2-Postiats-int-0.4.1.tgz. ###### Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) |
From: Hongwei Xi <gm...@gm...> - 2020-08-03 04:19:25
|
Hi, there, It is my pleasure to announce the release of ATS2-0.4.1. Note that this is the version needed (or may be needed in the future) for compiling the ongoing implementation of ATS3 (ATS/Xanadu). ------------------------------------------------ ATS-Postiats-0.4.1.tgz: The same as ATS-Postiats-int-0.4.1.tgz MD5: 99d99ea8296035abc7983fc3c21e1f05 SHA1: 1e1d2b33b2f89ca229689de6fc6b403d0d35b6fe -- ATS2-Postiats-gmp-1.4.0.tgz: MD5: 1f73c15ec2fcf0b6880f7a2b3d5da17c SHA1: af6a943b49236f02fcc1fe671477dbff85197c6a -- ATS2-Postiats-int-1.4.0.tgz: MD5: 6bbdd92aa412dd7f70a9e56363b8b22f SHA1: 6c9e4032514a297365ad1f92a17dd61ead70755f ------------------------------------------------ This is the 52nd release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ ###### Here is a list of major additions and changes since the last release: There are only a few minor modifications made to the last release; however, these modifications are needed for compiling ATS3 in the future. ###### Please note that there are two variants of the ATS2 package being released: The "gmp" variant depends on the GMP library and the "int" variant does not depend on the GMP library. In this release ATS2-Postiats-0.4.1.tgz is just the same as ATS2-Postiats-int-0.4.1.tgz. ###### Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) |
From: Chris D. <chr...@do...> - 2019-12-28 10:50:32
|
On Wed, Dec 25, 2019 at 3:58 PM Hongwei Xi <hw...@bu...> wrote: > 2. Introducing various keywords (e.g., atstflt, atsvtflt), which are > used in the implementation of ATS3(ATS/Xanadu) What do these keywords do, out of curiosity? -- https://bluishcoder.co.nz |
From: Hongwei Xi <hw...@bu...> - 2019-12-25 02:58:42
|
Hi, It is release time again :) It is my great pleasure to announce the release of ATS2-0.4.0. Note that this is the version needed for compiling ATS3 (ATS/Xanadu). First, many thanks to Brandon Barker for his generous agreement to taking over the duty of packaging and releasing ATS from this point on. Also, thanks to Richard Kent for assisting us. ------------------------------------------------ ATS-Postiats-0.4.0.tgz: MD5: ed0a8212b23c8ce281b5512eb0dd130f SHA1: f9a734b6d7040633d16a11c73f06175afe04482f ATS2-Postiats-gmp-0.4.0.tgz: MD5: 9ae8b64526affc951f33e189b20fa16f SHA1: 826d529830ba28581708a27c27952a9ed56f916e ATS2-Postiats-int-0.4.0.tgz: MD5: 3ed68ac11792be0689e43e9a6b3598c1 SHA1: fa41e400676cad30df6566770c4238fd02ecc6de ------------------------------------------------ By default, ATS-Postiats-0.4.0.tgz is no longer dependent on the GMP library. If you want a version of ATS-Postiats that uses GMP to solve integer constraints, please download ATS2-Postiats-gmp-0.4.0.tgz. ATS2-Positiats-int is just the same as ATS2-Positiats. ################################################ This is the 51st release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ Here is a list of major additions and changes since the last release: 1. Improving testing code: doc/EXAMPLE/ATSLF, doc/EXAMPLE/INTRO, doc/EXAMPLE/TESTATS Kudos to Artyom Shalkhakov! 2. Introducing various keywords (e.g., atstflt, atsvtflt), which are used in the implementation of ATS3(ATS/Xanadu) Please note that starting in this release, there are two variants of the package released: The "gmp" variant depends on the GMP library and the "int" variant does not depend on the GMP library. In this release ATS2-Postiats-0.4.0.tgz is just the same as ATS2-Postiats-int-0.4.0.tgz. Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) |
From: Hongwei Xi <hw...@bu...> - 2019-02-16 17:59:41
|
Hi, It is release time again :) It is my great pleasure to announce the release of ATS2-0.3.13. First, many thanks to Brandon Barker for his generous agreement to taking over the duty of packaging and releasing ATS from this point on. Also, thanks to Richard Kent for assisting us. Note that we plan to remove the dependency on the GMP library (in the default case) from the next release on. ------------------------------------------------ ATS2-Postiats-gmp-0.3.13.tgz: MD5: caf1515a077472b5cd56b92c996aec91 SHA1: 969fcaf9e2c11ca3b89d5b21aaff70f7b126a960 -- ATS2-Postiats-int-0.3.13.tgz: MD5: d67be4927beb144ad13bc9506c946859 SHA1: 442d51167cd82da0d7107dbbd16cc5b97d73b4b4 ------------------------------------------------ This is the 50th release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ Here is a list of major additions and changes since the last release: 1. Fixing the issue of escaping '$' in PHP string literals (atscc2php) Kudos to M88! 2. Fixing very minor issues in libats/qlist and libats/linmap 3. Enforcing that no d2var can be leaked/exported from a namespace Please note that starting in this release, there are two variants of the package released: the "gmp" variant depends on the GMP library. The "int" variant does not depend on the GMP library. In this release ATS2-Postiats-0.3.13.tgz is just the same as ATS2-Postiats-gmp-0.3.13.tgz. This is subject to change in future releases, as most users (especially new users) can get by without the extra dependency on GMP. Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) |
From: Hongwei Xi <hw...@bu...> - 2018-10-23 13:31:44
|
Hi, I am pleased to announce the release of ATS2-0.3.12. ###### First, many thanks to Brandon Barker for his generous agreement to taking over the duty of packaging and releasing ATS from this point on. ###### Also, I have started working on ATS3. For this point on, I do not forsee that major changes or features are to be added to ATS2 in the future (except library related stuff). Actually, ATS2 has already been very stable for the past couple of years. There will be future releases, albeit less and less frequently. ###### ATS2-Postiats-0.3.12.tgz: MD5: 6328cac96b0b0a19ecf13480662a7f42 SHA1: da6e20815351c6a59635ca61da9474c68fc06b34 ###### This is the 49th release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ Here is a list of major additions and changes since the last release: 1. Fixing parsing for hexidecimal floating point numbers (Thanks to Yannick Duchene!) 2. Fixing issues with some atsccomp transpilers and their libs 3. Tidying-up code for resolving fixity (xpushup and xreduce) 4. Atscc2js supports native records now (Kudos to AS-2018-08-18): See the function [emit_SELfltrec] for some detail. 5. Various-minor fixes of all sorts (e.g., on the prelude library) Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) |
From: David <da...@fr...> - 2018-06-11 12:24:40
|
Hi, Sorry for the previous email - I replied to the wrong ( old ) email. I have built source and binary ( x86_64 ) packages for CentOS 7.5 and Fedora 28. These were originally derived from Matthew Danish's packages. They are available at www.fractal.zone/downloads if anyone is interested in them. Regards David On Fri, 2018-06-08 at 22:33 -0400, Hongwei Xi wrote: > Hi, > > I am pleased to announce the release of ATS2-0.3.11. > > ###### > > First, many thanks to Brandon Barker for his generous > agreement to taking over the duty of packaging and releasing > ATS from this point on. Applause :) > > ###### > > Also, I have started working on ATS3. For this point on, > I do not forsee that major changes or features are to be > added to ATS2 in the future (except library related stuff). > Actually, ATS2 has already been very stable for the past couple > of years. There will be future releases, albeit less and less > frequently. > > ###### > ATS2-0.3.11.tgz: > MD5: 847b592ce92655fe72f68000104e12b4 > SHA1: c4df38d0ae759be4294c8a9d90f8bad7800dac50 > ###### > > This is the 48th release of ATS2, the successor of the ATS > programming language. The compiler for ATS2 is given the name > ATS/Positats, ATS2/Postiats or simply Postiats. > > The official website for ATS is: > > http://www.ats-lang.org > > ATS-Postiats is hosted at github: > > https://github.com/githwxi/ATS-Postiats > > Major releases of ATS2 are available at: > > https://sourceforge.net/projects/ats2-lang/ > > Major releases of external packages for ATS2 are available at: > > https://sourceforge.net/projects/ats2-lang-contrib/ > > ###### > > Cheers, > > --Hongwei > > Computer Science Department > Boston University > 111 Cummington Street > Boston, MA 02215 > > Email: hw...@cs... > Url: http://www.cs.bu.edu/~hwxi > Tel: +1 617 358 2511 (office) > Fax: +1 617 353 6457 (department) > > ###### > > Here is a list of major additions and changes since the last release: > > 1. Re-enabling the support for -IATS > 2. Rewording LICENSE: the ATS libraries are now covered under LGPLv3 > In particular, any C code generated by ATS/Postiats is NOT by > default > considered to be covered by the GPL/LGPL license of any kind. > 3. Renaming some keywords: > atstbox for atstype > atstflat for atst0ype > atsvtbox for atsvtype > atsvtflat for atsvt0ype > absimpl for assume and atsreimpl for reassume > > ------------------------------------------------------------------- > ----------- > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > _______________________________________________ > ats-lang-users mailing list > ats...@li... > https://lists.sourceforge.net/lists/listinfo/ats-lang-users |
From: David <da...@fr...> - 2018-06-11 12:19:41
|
Hi, I have built source and binary ( x86_64 ) packages for CentOS 7.5 and Fedora 28. These were originally derived from Matthew Danish's packages. They are available at www.fractal.zone/downloads if anyone is interested in them. Regards David On Sun, 2017-11-12 at 14:08 -0500, Hongwei Xi wrote: > Hi, > > I am pleased to announce the release of ATS2-0.3.8 > > This is the 45th release of ATS2, the successor of the > ATS programming language. The compiler for ATS2 is given > the name ATS/Positats, ATS2/Postiats or simply Postiats. > > The official website for ATS is: > > http://www.ats-lang.org > > ATS-Postiats is hosted at github: > > https://github.com/githwxi/ATS-Postiats > > Major releases of ATS2 are available at: > > https://sourceforge.net/projects/ats2-lang/ > > Major releases of external packages for ATS2 are available at: > > https://sourceforge.net/projects/ats2-lang-contrib/ > > ###### > > The following packages are included in this release: > > ###### > > ATS2-Postiats-0.3.8.tgz # requiring GMP > > MD5: 97ee260853a962895f5686e582b03bdb > SHA1: 5fcbf6fc13fbf0083564d26cf8e31dc13ae0d810 > > ###### > > ATS2-Postiats-contrib-0.3.8.tgz # contributed packages > ATS2-Postiats-include-0.3.8.tgz # CATS-files w/ MIT license. > > ###### > > I have included ATS2-Postiats-contrib (instead of releasing > it separately). From this point on, I will gradually merge parts > of ATS2-Postiats-contrib into ATS2-Postiats, and rely on external > package management systems (e.g., npm) to handle those that are > not selected for merging. > > After installing ATS-Postiats-include, one can compile the C code > generated from ATS source without installing the ATS compiler. So > a convenient way to distribute software written in ATS is to simply > release the C code generated from the ATS source. > > Please see below for some major additions and changes since the last > release (ATS2-0.3.7). > > Cheers, > > --Hongwei > > Computer Science Department > Boston University > 111 Cummington Street > Boston, MA 02215 > > Email: hw...@cs... > Url: http://www.cs.bu.edu/~hwxi > Tel: +1 617 358 2511 (office) > Fax: +1 617 353 6457 (department) > > ###################################################### > > Here is a list of major additions and changes since the last release: > > 1. Adding libatscc/ML/option0 > 2. Adding libatscc/ML/matrix0 > 3. Minorly improving libatscc/ML/list0 and libatscc/ML/array0 > 4. Fixing missing cases in eval1_p2at (pats_dmacro2_eval1.dats) > 5. Fixing and improving libats/funarray > 6. Adding calls to the_dynconlst_add to ensure that every exception > constructor is declared in the generated C code. > 7. Initiating building the "compiled" library libats/ML/COMPILE > 8. Fixing a glitch in compiling polymorphic functions that call > function templates (auxmat_env in [pats_ccomp_template.dats]) > A simple use case is found in doc/EXAMPLE/TESTATS/tempboxed.dats > 9. Adding support for calling variadic functions in a type-safe way. > There is no attempt to add support for type-safe implementation > of > variadic functions yet. > 10. Supporting the user of the flag --gc for myatscc. > > > ------------------------------------------------------------------- > ----------- > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > _______________________________________________ > ats-lang-users mailing list > ats...@li... > https://lists.sourceforge.net/lists/listinfo/ats-lang-users |
From: Hongwei Xi <hw...@bu...> - 2018-06-09 02:49:21
|
Hi, I am pleased to announce the release of ATS2-0.3.11. ###### First, many thanks to Brandon Barker for his generous agreement to taking over the duty of packaging and releasing ATS from this point on. Applause :) ###### Also, I have started working on ATS3. For this point on, I do not forsee that major changes or features are to be added to ATS2 in the future (except library related stuff). Actually, ATS2 has already been very stable for the past couple of years. There will be future releases, albeit less and less frequently. ###### ATS2-0.3.11.tgz: MD5: 847b592ce92655fe72f68000104e12b4 SHA1: c4df38d0ae759be4294c8a9d90f8bad7800dac50 ###### This is the 48th release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ ###### Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) ###### Here is a list of major additions and changes since the last release: 1. Re-enabling the support for -IATS 2. Rewording LICENSE: the ATS libraries are now covered under LGPLv3 In particular, any C code generated by ATS/Postiats is NOT by default considered to be covered by the GPL/LGPL license of any kind. 3. Renaming some keywords: atstbox for atstype atstflat for atst0ype atsvtbox for atsvtype atsvtflat for atsvt0ype absimpl for assume and atsreimpl for reassume |
From: Hongwei Xi <hw...@bu...> - 2018-03-22 03:07:21
|
Hi, I am pleased to announce the release of ATS2-0.3.10. ###### First, many thanks to Brandon Barker for his generous agreement to taking over the duty of packaging and releasing ATS from this point on. As a matter of fact, he helped a great deal package and release this version of ATS. Applause :) ###### ------------------------------------------------ ATS2-0.3.10.tgz: MD5: acb98ee91780cdde39c872203954d3b5 SHA1: 6a83800770cc50a7722c07e8c11122a901524ef8 ------------------------------------------------ This is the 47th release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ ###### The following two packages are in this release as well: ATS2-Postiats-contrib-0.3.10.tgz # contributed packages ATS2-Postiats-include-0.3.10.tgz # CATS-files w/ MIT license. After installing ATS-Postiats-include, one can compile the C code generated from ATS source without installing the ATS compiler. So a convenient way to distribute software written in ATS is to simply release the C code generated from the ATS source. Please see below for some major additions and changes since the last release (ATS2-0.3.9). ###### Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) ###### Here is a list of major additions and changes since the last release: 1. Improving atscntrb-sdstring and atscntrb-hx-cstream 2. Changing "atscntrb" to "atscntrb-hx" in the names of almost all of the npm-based ATS packages contributed by myself (Hongwei). This is a pervasive change due the wide use of these packages. 3. Adding libats/ML/SATS/argvec.sats and libats/ML/SATS/argvec.dats 4. Adding share/SCRIPT/buildRelease.sh to automate build/release ATS |
From: Hongwei Xi <hw...@bu...> - 2018-03-22 03:05:23
|
Hi, I am pleased to announce the release of ATS2-0.3.10. ###### First, many thanks to Brandon Barker for his generous agreement to taking over the duty of packaging and releasing ATS from this point on. As a matter of fact, he helped a great deal package and release this version of ATS. Applause :) ###### ------------------------------------------------ ATS2-0.3.10.tgz: MD5: acb98ee91780cdde39c872203954d3b5 SHA1: 6a83800770cc50a7722c07e8c11122a901524ef8 ------------------------------------------------ This is the 47th release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ ###### The following two packages are in this release as well: ATS2-Postiats-contrib-0.3.9.tgz # contributed packages ATS2-Postiats-include-0.3.9.tgz # CATS-files w/ MIT license. After installing ATS-Postiats-include, one can compile the C code generated from ATS source without installing the ATS compiler. So a convenient way to distribute software written in ATS is to simply release the C code generated from the ATS source. Please see below for some major additions and changes since the last release (ATS2-0.3.9). ###### Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) ###### Here is a list of major additions and changes since the last release: 1. Improving atscntrb-sdstring and atscntrb-hx-cstream 2. Changing "atscntrb" to "atscntrb-hx" in the names of almost all of the npm-based ATS packages contributed by myself (Hongwei). This is a pervasive change due the wide use of these packages. 3. Adding libats/ML/SATS/argvec.sats and libats/ML/SATS/argvec.dats 4. Adding share/SCRIPT/buildRelease.sh to automate build/release ATS |
From: Hongwei Xi <hw...@bu...> - 2018-03-22 03:04:05
|
Hi, I am pleased to announce the release of ATS2-0.3.10. ###### First, many thanks to Brandon Barker for his generous agreement to taking over the duty of packaging and releasing ATS from this point on. As a matter of fact, he helped a great deal package and release this version of ATS. Applause :) ###### ------------------------------------------------ ATS2-0.3.10.tgz: MD5: acb98ee91780cdde39c872203954d3b5 SHA1: 6a83800770cc50a7722c07e8c11122a901524ef8 ------------------------------------------------ This is the 47th release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ ###### The following two packages are in this release as well: ATS2-Postiats-contrib-0.3.9.tgz # contributed packages ATS2-Postiats-include-0.3.9.tgz # CATS-files w/ MIT license. After installing ATS-Postiats-include, one can compile the C code generated from ATS source without installing the ATS compiler. So a convenient way to distribute software written in ATS is to simply release the C code generated from the ATS source. Please see below for some major additions and changes since the last release (ATS2-0.3.9). ###### Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) ###### Here is a list of major additions and changes since the last release: 1. Improving atscntrb-sdstring and atscntrb-hx-cstream 2. Changing "atscntrb" to "atscntrb-hx" in the names of almost all of the npm-based ATS packages contributed by myself (Hongwei). This is a pervasive change due the wide use of these packages. 3. Adding libats/ML/SATS/argvec.sats and libats/ML/SATS/argvec.dats 4. Adding share/SCRIPT/buildRelease.sh to automate build/release ATS |
From: Andrei P. <and...@lr...> - 2018-03-06 13:25:41
|
******************************************************************************** VerifyThis Verification Competition 2018 CALL FOR PARTICIPATION -- TRAVEL GRANTS Competition to be held at ETAPS 2018 http://verifythis.ethz.ch ******************************************************************************** IMPORTANT DATES Grant application deadline: March 12, 2018 Competition: April 14 and 15, 2018 ABOUT VerifyThis 2018 is a program verification competition taking place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018) on April 14-15, 2018 in Thessaloniki, Greece. It is the 7th event in the VerifyThis competition series. The competition will offer a number of challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification. There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness, and elegance. PARTICIPATION: Participation is open for anybody interested. Teams of up to two people are allowed. Registration for ETAPS workshops and physical presence on site is required. We particularly encourage participation of: - student teams (this includes PhD students) - non-developer teams using a tool someone else developed - several teams using the same tool TRAVEL GRANTS: The competition has funds for a limited number of travel grants. A grant covers the incurred travel and accommodation costs up to a certain limit. The expected limit is EUR 350 for those coming from Europe and EUR 600 for those coming from outside Europe. To apply for a travel grant, send an email to ver...@cs... by March 12, 2018. The application should include: - your name - your affiliation - the verification system(s) you plan to use at the competition - the planned composition of your team - a short letter of motivation explaining your involvement with formal verification so far - if you are a student, please state the academic degree you are seeking and have your supervisor send a brief letter of support to ver...@cs... ORGANIZERS * Marieke Huisman, University of Twente, the Netherlands * Rosemary Monahan, Maynooth University, Ireland * Peter Müller, ETH Zürich, Switzerland * Andrei Paskevich, Paris-Sud University, France * Gidon Ernst, National Institute of Informatics Tokyo, Japan CONTACT Email: ver...@cs... Web: http://verifythis.ethz.ch |
From: Andrei P. <and...@lr...> - 2018-02-21 16:29:02
|
******************************************************************************* VerifyThis Verification Competition 2018 FIRST ANNOUNCEMENT AND CALL FOR PROBLEMS Competition to be held at ETAPS 2018 http://verifythis.ethz.ch ******************************************************************************** Get involved, even if you cannot participate in the competition: provide a challenge. IMPORTANT DATES Submission deadline: March 9, 2018 Competition: April 14 and 15, 2018 CALL FOR PROBLEMS To extend the problem pool, we are now soliciting algorithms and data structures which could contribute interesting verification challenges for the VerifyThis program verification competition (itself introduced below). We encourage suggestions at any level of detail, in particular submissions without a fully worked out verification task. - a problem may contain an informal statement of the algorithm to be implemented (optionally with complete or partial pseudocode) and the requirement(s) to be verified - a problem should be suitable for a 60-90 minute time slot - submission of reference solutions is welcome but not mandatory - problems with an inherent language- or tool-specific bias should be clearly identified as such - problems that contain several subproblems or other means of difficulty scaling are especially welcome - the organizers reserve the right (but no obligation) to use the problems in the competition, either as submitted or with modifications - submissions from (potential) competition participants are allowed Problems from previous competitions can be seen at http://verifythis.ethz.ch Submissions are to be sent by email to ver...@cs... by the date indicated above. PRIZES The most suitable submission for competition will receive a prize. ABOUT VerifyThis 2018 will take place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018) on April 14 and 15, 2018. It is the 7th event in the VerifyThis competition series. Information on previous events and participants can be found at http://verifythis.ethz.ch The aims of the competition are: - to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion - to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated by others. The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification. There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness and elegance. ORGANIZERS * Marieke Huisman, University of Twente, the Netherlands * Rosemary Monahan, Maynooth University, Ireland * Peter Müller, ETH Zürich, Switzerland * Andrei Paskevich, Paris-Sud University, France * Gidon Ernst, National Institute of Informatics Tokyo, Japan CONTACT Email: ver...@cs... Web: http://verifythis.ethz.ch |
From: Hongwei Xi <hw...@bu...> - 2018-01-15 16:47:03
|
Hi, I am pleased to announce the release of ATS2-0.3.9. This is the 46th release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ ###### The following packages are included in this release: ###### ATS2-Postiats-0.3.9.tgz # requiring GMP ------------------------------------------------ MD5: 89896a2ea58b07c2c409cd4297891aa1 SHA1: e350b7872cbac5ab1c3a539c7e35d176e39eb378 ------------------------------------------------ ###### ATS2-Postiats-contrib-0.3.9.tgz # contributed packages ATS2-Postiats-include-0.3.9.tgz # CATS-files w/ MIT license. ###### I have included ATS2-Postiats-contrib (instead of releasing it separately). From this point on, I will gradually merge parts of ATS2-Postiats-contrib into ATS2-Postiats, and rely on external package management systems (e.g., npm) to handle those that are not selected for merging. After installing ATS-Postiats-include, one can compile the C code generated from ATS source without installing the ATS compiler. So a convenient way to distribute software written in ATS is to simply release the C code generated from the ATS source. Please see below for some major additions and changes since the last release (ATS2-0.3.8). Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) ###################################################### Here is a list of major additions and changes since the last release: 1. Improving libatscc/libatscc2js regarding matrixref and matrix0 2. Improving doc/BOOK/ATS2FUNCRASH by tidying-up and fixing errors 3. Adding some examples in ATS-Tutoriats demonstrating ATS+ReactJS and ATS+React-Native 4. Adding basic programming support for parallelized stream-mapfold: ${PATSHOME}/libats/BUCS320/StreamPar (stream-processing) ${PATSHOME}/libats/BUCS520/StreamPar (linear-stream-processing) 5. Adding basic programming support for recursive directory-traversal: ${PATSHOME}/npm-utils/contrib/libats-hwxi/find_cli 6. Moving most higher-order functions from ATSPRE to ATSLIB/ML/atspre. This is a pervasive change, triggering a lot of (minor) fixes! 7. Rewriting several stream_vt functions to make them tail-recursive. 8. Moving ATSPRE/fcontainer and ATSPRE/giterator into libats/ATS2 9. Finishing EFFECTIVATS/SteamPar on streamization and stream-processing in parallel. 10. Starting the ATS-CodeBook project (at http://github.com/ats-lang): Hello, HX-intinf, ReadFromSTDIN, ReadFromSTDIN2, ReadFromSTDIN3, and WordFrqncyCount |
From: Hongwei Xi <hw...@bu...> - 2017-11-12 19:08:50
|
Hi, I am pleased to announce the release of ATS2-0.3.8 This is the 45th release of ATS2, the successor of the ATS programming language. The compiler for ATS2 is given the name ATS/Positats, ATS2/Postiats or simply Postiats. The official website for ATS is: http://www.ats-lang.org ATS-Postiats is hosted at github: https://github.com/githwxi/ATS-Postiats Major releases of ATS2 are available at: https://sourceforge.net/projects/ats2-lang/ Major releases of external packages for ATS2 are available at: https://sourceforge.net/projects/ats2-lang-contrib/ ###### The following packages are included in this release: ###### ATS2-Postiats-0.3.8.tgz # requiring GMP MD5: 97ee260853a962895f5686e582b03bdb SHA1: 5fcbf6fc13fbf0083564d26cf8e31dc13ae0d810 ###### ATS2-Postiats-contrib-0.3.8.tgz # contributed packages ATS2-Postiats-include-0.3.8.tgz # CATS-files w/ MIT license. ###### I have included ATS2-Postiats-contrib (instead of releasing it separately). From this point on, I will gradually merge parts of ATS2-Postiats-contrib into ATS2-Postiats, and rely on external package management systems (e.g., npm) to handle those that are not selected for merging. After installing ATS-Postiats-include, one can compile the C code generated from ATS source without installing the ATS compiler. So a convenient way to distribute software written in ATS is to simply release the C code generated from the ATS source. Please see below for some major additions and changes since the last release (ATS2-0.3.7). Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hw...@cs... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) ###################################################### Here is a list of major additions and changes since the last release: 1. Adding libatscc/ML/option0 2. Adding libatscc/ML/matrix0 3. Minorly improving libatscc/ML/list0 and libatscc/ML/array0 4. Fixing missing cases in eval1_p2at (pats_dmacro2_eval1.dats) 5. Fixing and improving libats/funarray 6. Adding calls to the_dynconlst_add to ensure that every exception constructor is declared in the generated C code. 7. Initiating building the "compiled" library libats/ML/COMPILE 8. Fixing a glitch in compiling polymorphic functions that call function templates (auxmat_env in [pats_ccomp_template.dats]) A simple use case is found in doc/EXAMPLE/TESTATS/tempboxed.dats 9. Adding support for calling variadic functions in a type-safe way. There is no attempt to add support for type-safe implementation of variadic functions yet. 10. Supporting the user of the flag --gc for myatscc. |