dbo:abstract
|
- ATS (Applied Type System) és un llenguatge de programació dissenyat per a la Universitat de Boston que incorpora "Tipus dependents de valors" i altres sistemes de tipus avançats així com construccions per assegurar la correcta finalització de les funcions entre les quals hi ha anotacions de mètrica i un sistema de proposicions i proves (predicats). El llenguatge parteix del cos del llenguatge ML Estàndard incorporant-hi construccions per a proveir els mecanismes avançats. (ca)
- ATS (Applied Type System) is a programming language designed to unify programming with formal specification. ATS has support for combining theorem proving with practical programming through the use of advanced type systems. A past version of The Computer Language Benchmarks Game has demonstrated that the performance of ATS is comparable to that of the C and C++ programming languages. By using theorem proving and strict type checking, the compiler can detect and prove that its implemented functions are not susceptible to bugs such as division by zero, memory leaks, buffer overflow, and other forms of memory corruption by verifying pointer arithmetic and reference counting before the program compiles. Additionally, by using the integrated theorem-proving system of ATS (ATS/LF), the programmer may make use of static constructs that are intertwined with the operative code to prove that a function attains its specification. (en)
- Applied Type System (ATS) ist eine Programmiersprache, die derzeit an der Universität Boston entwickelt wird. Der Schwerpunkt liegt auf einem ausdrucksstarken Typsystem mit Abhängigen Typen (Dependent Types) und Linearen Typen. Dieses ermöglicht unter anderem die Verifikation bestimmter Eigenschaften des Programms durch die explizite Konstruktion von Beweisen, sowie die Verwaltung von Ressourcen wie dynamisch allokiertem Speicher, geöffneten Dateien usw. Weitere Ziele sind eine gute Interoperabilität mit C, eine mit C vergleichbare Effizienz und die Eignung zur Systemprogrammierung. (de)
- ATS (Applied Type System) est un langage de programmation conçu pour unifier la programmation avec des spécifications formelles. ATS prend en charge la combinaison de la démonstration du théorème avec la programmation pratique grâce à l'utilisation de systèmes de type avancés . Une version antérieure de The Computer Language Benchmarks Game a démontré que les performances d'ATS sont comparables à celles des langages de programmation C et C++. En utilisant la preuve de théorème et la vérification de type stricte, le compilateur peut détecter et prouver que ses fonctions implémentées ne sont pas sensibles aux bogues tels que la division par zéro, les fuites de mémoire, le dépassement de mémoire tampon et d'autres formes de corruption de mémoire en vérifiant l' arithmétique du pointeur et le comptage de références avant que le programme se compile. De plus, en utilisant le système de démonstration de théorème intégré de l'ATS (ATS / LF), le programmeur peut utiliser des constructions statiques qui sont entrelacées avec le code opérationnel pour prouver qu'une fonction atteint sa spécification. (fr)
- ATS (от англ. Applied Type System) — язык программирования, нацеленный на поддержку формальной верификации в сочетании с практическим программированием с использованием системы зависимых типов. Разработчик — Хонвэй Си; основные конструкции заимствованы из ML и OCaml, предшествующий язык Dependent ML того же автора по сути включён в новый. Производительность программ на ATS сравнима с аналогичными показателями программ на Си и C++. По мнению автора языка эффективность для функциональных языков в основном зависит от способа представления данных в языке и оптимизации хвостовых вызовов, поэтому данные в ATS хранятся в простом (плоском) виде или преимущественно без вложенных представлений. (ru)
|
dbo:designer
| |
dbo:influencedBy
| |
dbo:latestReleaseDate
| |
dbo:latestReleaseVersion
| |
dbo:license
| |
dbo:thumbnail
| |
dbo:wikiPageExternalLink
| |
dbo:wikiPageID
| |
dbo:wikiPageLength
|
- 17053 (xsd:nonNegativeInteger)
|
dbo:wikiPageRevisionID
| |
dbo:wikiPageWikiLink
| |
dbp:designer
|
- Hongwei Xi at Boston University (en)
|
dbp:fileExt
| |
dbp:influencedBy
| |
dbp:latestReleaseDate
| |
dbp:latestReleaseVersion
| |
dbp:license
| |
dbp:logo
|
- File:The ATS Logo.svg (en)
|
dbp:name
| |
dbp:paradigm
| |
dbp:typing
| |
dbp:website
| |
dbp:wikiPageUsesTemplate
| |
dcterms:subject
| |
gold:hypernym
| |
rdf:type
| |
rdfs:comment
|
- ATS (Applied Type System) és un llenguatge de programació dissenyat per a la Universitat de Boston que incorpora "Tipus dependents de valors" i altres sistemes de tipus avançats així com construccions per assegurar la correcta finalització de les funcions entre les quals hi ha anotacions de mètrica i un sistema de proposicions i proves (predicats). El llenguatge parteix del cos del llenguatge ML Estàndard incorporant-hi construccions per a proveir els mecanismes avançats. (ca)
- Applied Type System (ATS) ist eine Programmiersprache, die derzeit an der Universität Boston entwickelt wird. Der Schwerpunkt liegt auf einem ausdrucksstarken Typsystem mit Abhängigen Typen (Dependent Types) und Linearen Typen. Dieses ermöglicht unter anderem die Verifikation bestimmter Eigenschaften des Programms durch die explizite Konstruktion von Beweisen, sowie die Verwaltung von Ressourcen wie dynamisch allokiertem Speicher, geöffneten Dateien usw. Weitere Ziele sind eine gute Interoperabilität mit C, eine mit C vergleichbare Effizienz und die Eignung zur Systemprogrammierung. (de)
- ATS (Applied Type System) is a programming language designed to unify programming with formal specification. ATS has support for combining theorem proving with practical programming through the use of advanced type systems. A past version of The Computer Language Benchmarks Game has demonstrated that the performance of ATS is comparable to that of the C and C++ programming languages. By using theorem proving and strict type checking, the compiler can detect and prove that its implemented functions are not susceptible to bugs such as division by zero, memory leaks, buffer overflow, and other forms of memory corruption by verifying pointer arithmetic and reference counting before the program compiles. Additionally, by using the integrated theorem-proving system of ATS (ATS/LF), the programme (en)
- ATS (Applied Type System) est un langage de programmation conçu pour unifier la programmation avec des spécifications formelles. ATS prend en charge la combinaison de la démonstration du théorème avec la programmation pratique grâce à l'utilisation de systèmes de type avancés . Une version antérieure de The Computer Language Benchmarks Game a démontré que les performances d'ATS sont comparables à celles des langages de programmation C et C++. En utilisant la preuve de théorème et la vérification de type stricte, le compilateur peut détecter et prouver que ses fonctions implémentées ne sont pas sensibles aux bogues tels que la division par zéro, les fuites de mémoire, le dépassement de mémoire tampon et d'autres formes de corruption de mémoire en vérifiant l' arithmétique du pointeur et le (fr)
- ATS (от англ. Applied Type System) — язык программирования, нацеленный на поддержку формальной верификации в сочетании с практическим программированием с использованием системы зависимых типов. Разработчик — Хонвэй Си; основные конструкции заимствованы из ML и OCaml, предшествующий язык Dependent ML того же автора по сути включён в новый. (ru)
|
rdfs:label
|
- ATS (llenguatge de programació) (ca)
- Applied Type System (de)
- ATS (programming language) (en)
- ATS (langage de programmation) (fr)
- ATS (язык программирования) (ru)
|
owl:sameAs
| |
prov:wasDerivedFrom
| |
foaf:depiction
| |
foaf:homepage
| |
foaf:isPrimaryTopicOf
| |
foaf:name
| |
foaf:page
| |
is dbo:influenced
of | |
is dbo:wikiPageDisambiguates
of | |
is dbo:wikiPageRedirects
of | |
is dbo:wikiPageWikiLink
of | |
is dbp:influenced
of | |
is foaf:primaryTopic
of | |