LINUX.ORG.RU
Новости — Open Source  

Coq 8.5

 ,


3

7

Тихо и незаметно вышла новая версия системы интерактивного доказательства теорем Coq (Петух).

Система Coq предоставляет язык Gallina (Курица) — функциональный язык с зависимыми типами, основанный на исчислении индуктивных конструкций. Особенностью данной системы является наличие особого подъязыка тактик доказательства (в отличии от, например, Агды, в которой пользователь конструирует элемент типа, являющийся доказательством, в явном виде с использованием интерактивного интерфейса, основанного на Emacs).

Coq используется как собственно в математике, так и для так называемого сертифицированного программирования — написания программ вместе с доказательством их корректности.

Основные новшества в версии 8.5:

  • асинхронное редактирование документов в CoqIDE, позволяющее работать с текущим доказательством, в то время как Coq проверяет другие доказательства в фоне;
  • полиморфизм относительно универсумов, позволяющий использовать одни и те же определения для универсумов разного уровня;
  • примитивные проекции, улучшающие временную и пространственную эффективность для записей и добавляющие для них эта-конверсию;
  • новый движок тактик;
  • новая процедура редукции native_compute, позволяющая вычислять термы, используя нативный компилятор OCaml'а;
  • новый быстрый режим компиляции, пропускающий проверку доказательств;
  • новая опция -type-in-type, позволяющая объединять иерархию типов в один универсум (делает логику несогласованной, но упрощает эксперименты);
  • заметное улучшение эффективности в целом.

>>> Новость

anonymous

Проверено: maxcom ()
Последнее исправление: Wizard_ (всего исправлений: 2)
← PulseAudio 8.0
TuxGuitar 1.3.0 →
Показаны ответы на комментарий. Показать все комментарии.
Ответ на: комментарий от d_a

выше уже слоубро кинули же статью из вики про вид джавагоспод

anonymous
()
Ответ на: комментарий от pacify

А еще есть это, толкько C#: 

using System;
namespace project5
{
    class Program
    {
        static void Main(string[] args)
        {
         
        }

        class Petux
        {
            private int petux = "kukareku!";
            
            public Petux():this(5)
            {
                
            }

            public Petux(int i):this()
            {
                
            }
        }

    }
}

OlegUP
()
Ответ на: комментарий от OlegUP

А еще есть это, толкько C#

Нее, шарп хороший. По сути шарп это то, чем должна была быть джава в идеальном мире. Жалко что народ попутал и везде поставил этот недошарп, в то время истинный шарп прозябает в роли, в которой должна была быть гавноджава. Если б я нашел работу на шарпе, я б туда с удовольствием пошел бы, а на джаву не приправленную груви, котлином или скалой смотреть противно.

q0tw4 ★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.
← PulseAudio 8.0
Open Source
TuxGuitar 1.3.0 →