Idris Programming Language

1–30 of 1695

0 selected

Sep 2

Call for Papers: Unsound - Sources of Unsoundness in Verification (Deadline Extension: 2022-09-16)

================================================================== Call for Papers Unsound: 1st

unread,

Call for Papers: Unsound - Sources of Unsoundness in Verification (Deadline Extension: 2022-09-16)

================================================================== Call for Papers Unsound: 1st

Sep 2

Vineet Kalghatgi

Aug 30

Trouble uninstalling Idris2 on M1 pro Mac

Hello Idris Team, I am trying to install Idris2 on an Apple silicon Mac(M1 Pro) and having trouble

unread,

Trouble uninstalling Idris2 on M1 pro Mac

Hello Idris Team, I am trying to install Idris2 on an Apple silicon Mac(M1 Pro) and having trouble

Aug 30

Holger Christensen

Aug 28

Parsing Idris 1

Hello I am writing a small parser for the Idris 1 language based on the documentation here: https://

unread,

Parsing Idris 1

Hello I am writing a small parser for the Idris 1 language based on the documentation here: https://

Aug 28

Steve Zdancewic

Aug 16

Certified Programs and Proofs (CPP) 2023 Call for Papers

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical

unread,

Certified Programs and Proofs (CPP) 2023 Call for Papers

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical

Aug 16

Jun 30

Call for Papers: Unsound - Sources of Unsoundness in Verification

================================================================== First Call for Papers Unsound: 1st

unread,

Call for Papers: Unsound - Sources of Unsoundness in Verification

================================================================== First Call for Papers Unsound: 1st

Jun 30

Steve Zdancewic

Jun 14

Certified Programs and Proofs (CPP) 2023: Call for Papers

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical

unread,

Certified Programs and Proofs (CPP) 2023: Call for Papers

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical

Jun 14

May 19

Idris2 + extensible records/row polymorphism/anonymous records ?

Ahoy! I am looking for a library which supports adhoc, extensible, anonymous records. Something like

unread,

Idris2 + extensible records/row polymorphism/anonymous records ?

Ahoy! I am looking for a library which supports adhoc, extensible, anonymous records. Something like

May 19

Apr 26

Position of Lecturer or Senior Lecturer in Cybersecurity at University of Sheffield

Greetings, The Department of Computer Science at University of Sheffield has an open position of

unread,

Position of Lecturer or Senior Lecturer in Cybersecurity at University of Sheffield

Greetings, The Department of Computer Science at University of Sheffield has an open position of

Apr 26

Attila Lendvai, Edwin Brady8

Apr 14

FTR, i've filed some patches for Guix that can bootstrap the Idris2 package all the way down from

unread,

FTR, i've filed some patches for Guix that can bootstrap the Idris2 package all the way down from

Apr 14

andre....@gmail.com

Apr 11

Idris Developer Meeting May 2022

Dear Idris enthusiasts, The next Idris developer meeting is scheduled for the 16th of May and will

unread,

Idris Developer Meeting May 2022

Dear Idris enthusiasts, The next Idris developer meeting is scheduled for the 16th of May and will

Apr 11

Mar 25

Which Emacs mode for Idris 2?

Hi all, after a long time staying away from Idris it's time to give it another try. I would like

unread,

Which Emacs mode for Idris 2?

Hi all, after a long time staying away from Idris it's time to give it another try. I would like

Mar 25

Mar 6

22nd Midlands Graduate School, 10-14 April 2022: Call for Participation

CALL FOR PARTICIPATION 22nd Midlands Graduate School (MGS'22) in the Foundations of Computing

unread,

22nd Midlands Graduate School, 10-14 April 2022: Call for Participation

CALL FOR PARTICIPATION 22nd Midlands Graduate School (MGS'22) in the Foundations of Computing

Mar 6

Mar 3

PhD Position in Number Theory and Formalization

The Department of Mathematics of Vrije Universiteit Amsterdam welcomes applications for a fully-

unread,

PhD Position in Number Theory and Formalization

The Department of Mathematics of Vrije Universiteit Amsterdam welcomes applications for a fully-

Mar 3

andre....@gmail.com

Feb 24

Presentation about GRIN on discord

Hello everyone, This Sunday at 3:30 UTC+0 there will be a presentation about the Idris2 GRIN backend.

unread,

Presentation about GRIN on discord

Hello everyone, This Sunday at 3:30 UTC+0 there will be a presentation about the Idris2 GRIN backend.

Feb 24

Nicolas Alexander Schmidt, Stefan Höck2

Jan 31

Getting the default implementation of an interface

Does `%search` what you want to do? On Mon, Jan 31, 2022 at 11:15:22AM +0100, Nicolas Alexander

unread,

Getting the default implementation of an interface

Does `%search` what you want to do? On Mon, Jan 31, 2022 at 11:15:22AM +0100, Nicolas Alexander

Jan 31

Jan 17

Written in Idris2: a demo of non-Euclidean geometry using WebGL

On Tue, Jan 18, 2022 at 04:43:44AM +0000, James Cook wrote: > I just published something I had a

unread,

Written in Idris2: a demo of non-Euclidean geometry using WebGL

On Tue, Jan 18, 2022 at 04:43:44AM +0000, James Cook wrote: > I just published something I had a

Jan 17

Jorge Gomez Abrante

Jan 16

Guile Code Generator

Hi, Is anyone working on a Guile Code Generator for Idris?

unread,

Guile Code Generator

Hi, Is anyone working on a Guile Code Generator for Idris?

Jan 16

mmhell...@gmail.com

Jan 2

Idris 2 0.5.1 for JVM

Hello everyone, I am happy to announce that Idris 2 JVM backend has finally caught up to Idris 2

unread,

Idris 2 0.5.1 for JVM

Hello everyone, I am happy to announce that Idris 2 JVM backend has finally caught up to Idris 2

Jan 2

apostolis.xe...@gmail.com, Nathan Ringo5

Jan 2

perceus reference counting - dependent types without a garbage collector?

Main_ones is a function that produces a stream of ones. You need to look at the memory as it is

unread,

perceus reference counting - dependent types without a garbage collector?

Main_ones is a function that produces a stream of ones. You need to look at the memory as it is

Jan 2

tony mailer, Denis Buzdalov3

12/31/21

Error about negative Nat

Ah, gotcha. Thanks for the detailed explanation. On Thursday, December 30, 2021 at 8:50:44 PM UTC-5

unread,

Error about negative Nat

Ah, gotcha. Thanks for the detailed explanation. On Thursday, December 30, 2021 at 8:50:44 PM UTC-5

12/31/21

12/28/21

Any way to speed up Data.Fin conversions, e.g. strengthen, fromInteger?

On the other hand, strengthen, fromInteger and finToInteger all seem to take O(n) time. Is there a

unread,

Any way to speed up Data.Fin conversions, e.g. strengthen, fromInteger?

On the other hand, strengthen, fromInteger and finToInteger all seem to take O(n) time. Is there a

12/28/21

Jan de Muijnck-Hughes, James Cook2

12/22/21

Community Announcements are also made on Discord...

> I have asked the admins for this Discord community to ensure that all > 'Community

unread,

Community Announcements are also made on Discord...

> I have asked the admins for this Discord community to ensure that all > 'Community

12/22/21

12/17/21

IJCAR 2022 - Call for Papers

IJCAR 2022 - Call for Papers https://easychair.org/smart-program/IJCAR2022/. ***Important Dates***

unread,

IJCAR 2022 - Call for Papers

IJCAR 2022 - Call for Papers https://easychair.org/smart-program/IJCAR2022/. ***Important Dates***

12/17/21

12/8/21

Certified Programs and Proofs (CPP) 2022: Call for Participation

*** Call for Participation *** *** Certified Programs and Proofs (CPP) 2022 *** - Early registration

unread,

Certified Programs and Proofs (CPP) 2022: Call for Participation

*** Call for Participation *** *** Certified Programs and Proofs (CPP) 2022 *** - Early registration

12/8/21

Wind R, Denis Buzdalov2

11/30/21

Trouble proving mult n 0 = 0

вт, 30 нояб. 2021 г. в 23:41, 'Wind R' via Idris Programming Language <idris-lang@

unread,

Trouble proving mult n 0 = 0

вт, 30 нояб. 2021 г. в 23:41, 'Wind R' via Idris Programming Language <idris-lang@

11/30/21

James Cook, … Denis Buzdalov22

10/8/21

Any way to work around Javascript stack size limit?

I'm finally getting back to this. After some experimentation, I think it's not actually the

unread,

Any way to work around Javascript stack size limit?

I'm finally getting back to this. After some experimentation, I think it's not actually the

10/8/21

10/7/21

post-doctoral research position - Effect Handler Oriented Programming - Edinburgh

Hi, I have an opening for a post-doctoral research position at The University of Edinburgh on Effect

unread,

post-doctoral research position - Effect Handler Oriented Programming - Edinburgh

Hi, I have an opening for a post-doctoral research position at The University of Edinburgh on Effect

10/7/21

Tornai, … Denis Buzdalov3

9/28/21

Enforcing a binary search tree ordering in the data type

`Ord` is particularly painful to work with in the proof-world setting. First, it has a lot of

unread,

Enforcing a binary search tree ordering in the data type

`Ord` is particularly painful to work with in the proof-world setting. First, it has a lot of

9/28/21

James Cook, … Denis Buzdalov10

9/26/21

Idris2: How to specify named implementation as input to default implementation?

Much better, thanks! Maybe I will continue to use it, since it's not too bad. On Monday, 27

unread,

Idris2: How to specify named implementation as input to default implementation?

Much better, thanks! Maybe I will continue to use it, since it's not too bad. On Monday, 27

9/26/21

9/18/21

Idris 2 version 0.5.0 released

Dear all, Idris 2 version 0.5.0 has been released. You can find full details, including all the

unread,

Idris 2 version 0.5.0 released

Dear all, Idris 2 version 0.5.0 has been released. You can find full details, including all the

9/18/21

Search

Clear search

Close search

Google apps

Main menu