This HTML5 document contains 198 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n19http://uz.dbpedia.org/resource/
dctermshttp://purl.org/dc/terms/
yago-reshttp://yago-knowledge.org/resource/
n21http://idris-lang.org/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
dbpedia-cahttp://ca.dbpedia.org/resource/
n26https://global.dbpedia.org/id/
yagohttp://dbpedia.org/class/yago/
dbthttp://dbpedia.org/resource/Template:
schemahttp://schema.org/
dbpedia-ruhttp://ru.dbpedia.org/resource/
rdfshttp://www.w3.org/2000/01/rdf-schema#
freebasehttp://rdf.freebase.com/ns/
n11http://hackage.haskell.org/package/
dbpedia-fahttp://fa.dbpedia.org/resource/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
dbpedia-zhhttp://zh.dbpedia.org/resource/
wikipedia-enhttp://en.wikipedia.org/wiki/
dbphttp://dbpedia.org/property/
dbchttp://dbpedia.org/resource/Category:
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
n27http://docs.idris-lang.org/en/latest/
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/
dbpedia-rohttp://ro.dbpedia.org/resource/

Statements

Subject Item
dbr:Proof_assistant
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:List_of_arbitrary-precision_arithmetic_software
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Dependent_type
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Applicative_functor
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Per_Martin-Löf
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Induction-recursion
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Intuitionistic_type_theory
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:List_of_programming_languages
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:List_of_programming_languages_by_type
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Substructural_type_system
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Coq
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Rust_(programming_language)
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Generational_list_of_programming_languages
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Clean_(programming_language)
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
dbp:influenced
dbr:Idris_(programming_language)
dbo:influenced
dbr:Idris_(programming_language)
Subject Item
dbr:Epigram_(programming_language)
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
dbp:influenced
dbr:Idris_(programming_language)
dbo:influenced
dbr:Idris_(programming_language)
Subject Item
dbr:Whitespace_(programming_language)
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:ML_(programming_language)
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
dbp:influenced
dbr:Idris_(programming_language)
dbo:influenced
dbr:Idris_(programming_language)
Subject Item
dbr:Comparison_of_functional_programming_languages
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Timeline_of_programming_languages
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Agda_(programming_language)
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
dbp:influenced
dbr:Idris_(programming_language)
Subject Item
dbr:Algebraic_data_type
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:History_of_software
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Haskell
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
dbo:influenced
dbr:Idris_(programming_language)
Subject Item
dbr:Iosevka
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Ivor_the_Engine
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Referential_transparency
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Idris_(programming_language)
rdf:type
dbo:ProgrammingLanguage wikidata:Q315 yago:ArtificialLanguage106894544 wikidata:Q9143 owl:Thing dbo:Software dbo:Language yago:Communication100033020 schema:Language yago:WikicatFunctionalLanguages yago:Abstraction100002137 yago:Language106282651 yago:WikicatDependentlyTypedLanguages yago:ProgrammingLanguage106898352
rdfs:label
Idris (язык программирования) Idris Idris (llenguatge de programació) Idris (programming language)
rdfs:comment
Idris és un llenguatge de programació funcional amb tipus dependents de valors, desenvolupat a la Universitat escocesa de Saint Andrews sota la direcció d'. per a aplicacions de propòsit general amb la possibilitat de verificació estàtica incorporada. El sistema de tipus és similar al del llenguatge , amb una sintaxi molt semblant al Haskell però amb semàntica estricta (avaluació primerenca), designant l'avaluació tardana als tipus (tipus Lazy a). Els tipus hi són objectes de primer ordre, permetent barrejar objectes i tipus als paràmetres i resultats. Idris是一个通用的依赖类型纯函数式编程语言,其类型系统与Agda以及相似。 Idris语言具备堪与Coq媲美的交互式定理证明能力,自带tactics,而其设计目标侧重于通用系统编程更甚于辅助证明。Idris的其他设计目标还包括“可观的”代码性能,对副作用的控制,以及对于实现嵌入式领域特定语言(Embedded Domain Specific Language,EDSL)的支持。 Idris通过一个依赖类型的核心语言TT生成C语言的中间代码并编译到本地机器码,并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java和LLVM的编译器后端。 Idris的名字来自于20世纪70年代的英国儿童动画片《》里,一条会唱歌的龙。 Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but it is designed to be a general-purpose programming language similar to Haskell. Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine. Idris — чистый функциональный язык программирования общего назначения с Haskell-подобным синтаксисом и поддержкой зависимых типов. Система типов подобна системе типов языка Agda. Язык поддерживает средства автоматического доказательства, сравнимые с Coq, включая поддержку тактик, однако фокусируется не на них, а позиционируется как . Цели его создания: «достаточная» производительность, простота управления побочными эффектами и средства реализации встраиваемых предметно-ориентированных языков. Язык назван в честь поющего дракона Идриса из британской детской телепередачи 1970 года .
foaf:name
Idris
dbp:name
Idris
dcterms:subject
dbc:Haskell_programming_language_family dbc:Functional_languages dbc:Pattern_matching_programming_languages dbc:Free_compilers_and_interpreters dbc:Software_using_the_BSD_license dbc:Cross-platform_free_software dbc:Experimental_programming_languages dbc:Free_software_programmed_in_Haskell dbc:Programming_languages_created_in_2007 dbc:Dependently_typed_languages dbc:2007_software dbc:High-level_programming_languages
dbo:wikiPageID
39035048
dbo:wikiPageRevisionID
1050140606
dbo:wikiPageWikiLink
dbr:Termination_analysis dbr:EDSL dbr:Type_class dbr:Node.js dbr:Dependent_type dbc:Haskell_programming_language_family dbr:Programming_language dbr:Generalized_algebraic_data_type dbr:JavaScript dbc:Functional_languages dbc:Pattern_matching_programming_languages dbr:Compile_time dbr:Scheme_(programming_language) dbr:Linear_type_system dbr:Side_effect_(computer_science) dbr:Self-hosting_(compilers) dbr:Lazy_evaluation dbr:Clean_(programming_language) dbr:ML_(programming_language) dbr:C_(programming_language) dbr:Cross-platform dbc:Cross-platform_free_software dbc:Free_compilers_and_interpreters dbc:Software_using_the_BSD_license dbc:Experimental_programming_languages dbr:Haskell_(programming_language) dbc:Programming_languages_created_in_2007 dbr:Array_data_structure dbr:Quantitative_type_theory dbr:F_Sharp_(programming_language) dbr:Haskell_98 dbc:Free_software_programmed_in_Haskell dbc:Dependently_typed_languages dbr:Partial_function dbr:Cheney's_algorithm dbr:Coq dbr:Tactic_(computer_science) dbr:Library_(computing) dbr:General-purpose_programming_language dbr:BSD_licenses dbr:LLVM dbr:Type_checking dbr:Purely_functional_programming dbr:Infinite_loop dbr:Hello_world_program dbr:Parametric_polymorphism dbr:Rust_(programming_language) dbr:Ivor_the_Engine dbr:Subroutine dbr:Total_functional_programming dbr:Common_Intermediate_Language dbc:High-level_programming_languages dbc:2007_software dbr:Functional_programming dbr:Inductively-defined_data_type dbr:Proof_assistant dbr:Type_signature dbr:Agda_(programming_language) dbr:Type_system dbr:Epigram_(programming_language) dbr:Garbage_collection_(computer_science) dbr:Java_virtual_machine
dbo:wikiPageExternalLink
n11:idris n21: n27:index.html
owl:sameAs
wikidata:Q15408477 dbpedia-ru:Idris_(язык_программирования) dbpedia-fa:ادریس_(زبان_برنامه‌نویسی) freebase:m.0swpzmh dbpedia-ca:Idris_(llenguatge_de_programació) n19:Idris_(dasturlash_tili) yago-res:Idris_(programming_language) dbpedia-ro:Idris_(limbaj_de_programare) dbpedia-zh:Idris n26:YN58
dbp:wikiPageUsesTemplate
dbt:Vague dbt:Infobox_programming_language dbt:Primary_sources dbt:URL dbt:Start_date_and_age dbt:Programming_languages dbt:Reflist
dbp:designer
Edwin Brady
dbp:influencedBy
dbr:Clean_(programming_language) dbr:Coq dbr:ML_(programming_language) dbr:Rust_(programming_language) dbr:Epigram_(programming_language) dbr:Haskell_(programming_language) dbr:Agda_(programming_language) dbr:F_Sharp_(programming_language)
dbp:latestReleaseDate
2020-05-24
dbp:latestReleaseVersion
1.3
dbp:license
dbr:BSD_licenses
dbp:operatingSystem
dbr:Cross-platform
dbp:paradigm
dbr:Functional_programming
dbo:abstract
Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but it is designed to be a general-purpose programming language similar to Haskell. The Idris type system is similar to Agda's, and proofs are similar to Coq's, including (theorem proving functions/procedures) via elaborator reflection. Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages. Idris compiles to C (relying on a custom copying garbage collector using Cheney's algorithm) and JavaScript (both browser- and Node.js-based). There are third-party code generators for other platforms, including JVM, CIL, and LLVM. Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine. Idris — чистый функциональный язык программирования общего назначения с Haskell-подобным синтаксисом и поддержкой зависимых типов. Система типов подобна системе типов языка Agda. Язык поддерживает средства автоматического доказательства, сравнимые с Coq, включая поддержку тактик, однако фокусируется не на них, а позиционируется как . Цели его создания: «достаточная» производительность, простота управления побочными эффектами и средства реализации встраиваемых предметно-ориентированных языков. Реализован на Haskell, доступен в виде -пакета. Исходный код на Idris компилируется в набор промежуточных представлений, а из них — в си-код, при исполнении которого используется копирующий сборщик мусора с применением . Также официально реализована возможность компиляции в код на JavaScript (в том числе для Node.js). Существуют сторонние реализации кодогенераторов для Java, JVM, CIL, Erlang, PHP и (с ограничением) LLVM. Язык назван в честь поющего дракона Идриса из британской детской телепередачи 1970 года . Язык сочетает особенности основных популярных языков функционального программирования с возможностями, заимствованными из систем автоматического доказательства, фактически размывая границу между этими двумя классами языков. Вторая версия языка (выпущенная в 2020 году, основанная на «количественной теории типов») существенно отличается от первой: добавлена полноценная поддержка , код компилируется по умолчанию в Scheme, компилятор языка написан на самом языке. Idris是一个通用的依赖类型纯函数式编程语言,其类型系统与Agda以及相似。 Idris语言具备堪与Coq媲美的交互式定理证明能力,自带tactics,而其设计目标侧重于通用系统编程更甚于辅助证明。Idris的其他设计目标还包括“可观的”代码性能,对副作用的控制,以及对于实现嵌入式领域特定语言(Embedded Domain Specific Language,EDSL)的支持。 Idris通过一个依赖类型的核心语言TT生成C语言的中间代码并编译到本地机器码,并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java和LLVM的编译器后端。 Idris的名字来自于20世纪70年代的英国儿童动画片《》里,一条会唱歌的龙。 Idris és un llenguatge de programació funcional amb tipus dependents de valors, desenvolupat a la Universitat escocesa de Saint Andrews sota la direcció d'. per a aplicacions de propòsit general amb la possibilitat de verificació estàtica incorporada. El sistema de tipus és similar al del llenguatge , amb una sintaxi molt semblant al Haskell però amb semàntica estricta (avaluació primerenca), designant l'avaluació tardana als tipus (tipus Lazy a). Els tipus hi són objectes de primer ordre, permetent barrejar objectes i tipus als paràmetres i resultats. Aquest llenguatge permet incorporar tipus com a proposicions i funcions com a proves, per certificar les propietats de la funcionalitat aportada, seguint la teoria de la Correspondència Curry-Howard entre programes i proves, incorporant propietats dels sistemes d'ajuda a la comprovació (Proof assistants) també anomenats com ara , o bé .
dbp:fileExt
.idr, .lidr
dbp:latestTestDate
2021-09-20
dbp:latestTestVersion
0.5
prov:wasDerivedFrom
wikipedia-en:Idris_(programming_language)?oldid=1050140606&ns=0
dbo:wikiPageLength
10002
dbo:latestReleaseDate
2020-05-24
dbo:latestReleaseVersion
1.3.3
dbo:influencedBy
dbr:Coq dbr:Haskell_(programming_language) dbr:Epigram_(programming_language) dbr:F_Sharp_(programming_language) dbr:ML_(programming_language) dbr:Clean_(programming_language) dbr:Rust_(programming_language) dbr:Agda_(programming_language)
dbo:license
dbr:BSD_licenses
foaf:isPrimaryTopicOf
wikipedia-en:Idris_(programming_language)
Subject Item
dbr:Idris_2
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
dbo:wikiPageRedirects
dbr:Idris_(programming_language)
Subject Item
dbr:Idris
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
dbo:wikiPageDisambiguates
dbr:Idris_(programming_language)
Subject Item
dbr:Self-hosting_(compilers)
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:First-class_citizen
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Uniqueness_type
dbo:wikiPageWikiLink
dbr:Idris_(programming_language)
Subject Item
dbr:Agda_(programming_language)__Agda__1
dbo:influenced
dbr:Idris_(programming_language)
Subject Item
wikipedia-en:Idris_(programming_language)
foaf:primaryTopic
dbr:Idris_(programming_language)