ALF (proof assistant)

For the programming language, see Algebraic Logic Functional programming language.

ALF ("Another logical framework") is a structure editor for monomorphic Martin-Löf type theory developed at Chalmers University. It is a predecessor of the Alfa, Agda, Cayenne and Coq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.[1][2]

References

  1. ^ Thierry Coquand (1992). "Pattern Matching with Dependent Types". In Bengt Nordström, Kent Petersson, and Gordon Plotkin (editors), Electronic Proceedings of the Third Annual BRA Workshop on Logical Frameworks (Båstad, Sweden).
  2. ^ Thorsten Altenkirch, Conor McBride and James McKinna (2005). "Why Dependent Types Matter".

Further reading


Stub icon

This computer science article is a stub. You can help Wikipedia by expanding it.

Read other articles:

Lin Sen

Chairman of the National Government of China from 1938-1943 Lin Sen林森Chairman of the National Government of ChinaIn office15 December 1931 – 1 August 1943PremierChen Mingshu (acting)Sun FoWang JingweiChiang Kai-shekH.H. KungMilitary chiefChiang Kai-shekPreceded byChiang Kai-shekSucceeded byChiang Kai-shek (acting)President of the Legislative YuanIn office2 March 1931 – 1 January 1932Vice PresidentShao YuanchongPreceded byHu HanminSucceeded byShao Yuanchong (acting)Zh...

 

Abierto Tampico

Abierto Tampico Datos generalesSede TampicoMéxico MéxicoRecinto Ciudad Deportiva de TampicoCategoría WTA 125KSuperficie Dura / ExteriorCuadro 32S / 16SQ / 16DOrganizador WTAPremio US$ 115.000 Sitio oficial [editar datos en Wikidata] El Abierto de Tenis de Tampico es un torneo profesional femenil, que se celebra anualmente a finales de octubre. El torneo se encuentra dentro de las actividades realizadas por la WTA dentro del circuito mundial 125K Series. El torneo perteneció del ...

 

1974 smallpox epidemic in India

Disease outbreak in India Map of India with states. The 1974 smallpox epidemic in India infected 188,000 people, leading to the deaths of 31,000 Indians.[1] The media reported the smallpox epidemic as the most severe.[2] However, the claim is debatable due to improvements in reporting since the epidemics of 1875 and 1967.[3] The 1974 epidemic occurred during the country’s intensified campaign against the virus, which saw a shift in strategy from mass vaccinations to ...

The African Queen (film)

1951 film by John Huston For the 1977 television film, see The African Queen (1977 film). The African QueenUS theatrical release posterDirected byJohn HustonScreenplay byJohn HustonJames AgeePeter ViertelJohn CollierBased onThe African Queen1935 novelby C. S. ForesterProduced bySam SpiegelJohn Woolf (uncredited)StarringHumphrey BogartKatharine HepburnRobert MorleyCinematographyJack CardiffEdited byRalph KemplenMusic byAllan GrayProductioncompaniesHorizon PicturesRomulus Films[1]Distri...

 

2010–11 NCAA Division I men's ice hockey season

2010–11 NCAA Division I men's ice hockey seasonThe Xcel Energy Center in Saint Paul, Minnesota hosted the 2011 Frozen FourDurationOctober 2, 2010–April 9, 2011NCAA tournament2011National championshipXcel Energy CenterSaint Paul, MinnesotaNCAA championMinnesota–DuluthHobey Baker AwardAndy Miele(Miami) List of NCAA Division I men's ice hockey seasons ← 2009–10 2011–12 → The 2010–11 NCAA Division I men's ice hockey season began on October 2, 2010 and co...

 

An・an

この項目では、ファッション雑誌について説明しています。その他の用法については「アンアン」をご覧ください。 この記事は検証可能な参考文献や出典が全く示されていないか、不十分です。出典を追加して記事の信頼性向上にご協力ください。（このテンプレートの使い方）出典検索?: An・an – ニュース · 書籍 · スカラー · CiNii · J-STAGE&...

Качурка чорна

?Качурка чорна Охоронний статус Найменший ризик (МСОП 3.1)[1] Біологічна класифікація Домен: Еукаріоти (Eukaryota) Царство: Тварини (Animalia) Тип: Хордові (Chordata) Клас: Птахи (Aves) Ряд: Буревісникоподібні (Procellariiformes) Родина: Качуркові (Hydrobatidae) Рід: Вилохвоста качурка (Oceanodroma) Вид: Ка...

 

Nat Clifton

American basketball player and coach This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Nat Clifton – news · newspapers · books · scholar · JSTOR (October 2006) (Learn how and when to remove this template message) Nat CliftonPersonal informationBorn(1922-10-13)October 13, 1922England, Arkansas, U.S.DiedAugust 3...

 

Sugar (Stanley Turrentine album)

1970 studio album by Stanley TurrentineSugarStudio album by Stanley TurrentineReleasedNovember 22, 1970[1]RecordedNovember 1970 (#1-4)Van Gelder Studio, Englewood CliffsJuly 18, 1971 (#5)Hollywood Palladium, Los AngelesGenreJazz, Soul jazz, Hard bopLength44:40 original LPLabelCTICTI 6005ProducerCreed TaylorStanley Turrentine chronology Another Story(1969) Sugar(1970) The Sugar Man(1971) Sugar is an album by jazz saxophonist Stanley Turrentine, his first recorded for the CTI Re...

Праліси і квазіпраліси Лопухівського лісництва

Праліси і квазіпраліси Лопухівського лісництва(пам'ятка природи) 48°17′26″ пн. ш. 24°03′06″ сх. д. / 48.29056° пн. ш. 24.05167° сх. д. / 48.29056; 24.05167Координати: 48°17′26″ пн. ш. 24°03′06″ сх. д. / 48.29056° пн. ш. 24.05167° сх. д. / 48.29056; 24.05167

 

Predefinição:Política da Chéquia

Parte da série sobrePolítica da Chéquia Constituição Executivo Presidente Petr Pavel Primeiro-ministro (Lista) Petr Fiala Legislativo Parlamento da Chéquia Senado Câmara dos Deputados Judiciário Suprema Corte Tribunal Constitucional Eleições Eleições presidenciais 1993  • 1998  • 2003  • 2008  • 2013  • 2018  • 2023 Eleições legislativas 1992  • 1996  • 1998  • 2002  • 2006  • 2010  • 2013  ...

 

لقاس (ردمان)

قرية لقاس  - قرية -  تقسيم إداري البلد  اليمن المحافظة محافظة البيضاء المديرية مديرية ردمان العزلة عزلة ردمان ال عوض السكان التعداد السكاني 2004 السكان 364   • الذكور 180   • الإناث 184   • عدد الأسر 31   • عدد المساكن 33 معلومات أخرى التوقيت توقيت اليمن (+3 غرين...

Heinz Heger

Josef Kohout (24 January 1915 – 15 March 1994) was an Austrian Nazi concentration camp survivor, imprisoned for his homosexuality. He is best known for the 1972 book Die Männer mit dem rosa Winkel (The Men With the Pink Triangle), which was written by his acquaintance Hans Neumann using the pen name Heinz Heger, which is often falsely attributed to Kohout.[1] The book is one of very few first-hand accounts of the treatment of homosexuals in Nazi imprisonment. It has been translated...

 

عين الغزال (فيلم)

عين الغزاللقطة من الفيلممعلومات عامةالصنف الفني روائيتاريخ الصدور 1924[1]مدة العرض 17 دقيقة[2]اللغة الأصلية ‍العربيةالعرض أبيض وأسود البلد  تونسالطاقمالمخرج ألبير شمامة شيكليالبطولة هايدي تمزالي, أحمد دزيري, عبد القاسم بن طالب, حاج هادي دهاليتعديل - تعديل مصدري - ...

 

Kongres Amerika Serikat ke-22

Kongres Amerika Serikat c22United States Capitol (1827)Periode4 Maret 1831 – 4 Maret 1833Anggota48 senator213 anggota dewan3 delegasi tanpa suaraMayoritas SenatJacksonPresiden SenatJohn C. Calhoun (1831–1832)Kosong (1832–1833)Mayoritas DPRJacksonKetua DPRAndrew StevensonPres. Senat Pro TemporeSamuel SmithLittleton TazewellHugh L. WhiteSesike-1: 5 Desember 1831 – 16 Juli 1832ke-2: 3 Desember 1832 – 2 Maret 1833ke-21 ←→ ke-23 Kongres Amerika Serikat Kedua Puluh Dua ...

Urun daya dalam pemilihan umum Presiden Indonesia 2014

Infografik kelompok-kelompok relawan urun daya pada Pilpres 2014. Urun daya dalam Pilpres 2014 merupakan bentuk partisipasi masyarakat berbasis data terbuka pada Pemilihan Umum Presiden Indonesia 2014 dengan memanfaatkan data yang dirilis oleh Komisi Pemilihan Umum (KPU). Sejarah Kebijakan Data Terbuka Salah satu komitmen Indonesia sebagai penggagas Open Government Partnership pada tahun 2011 adalah menerapkan Kebijakan Data Terbuka pada pelaksanaan Pemilihan Umum Legislatif dan Pemilihan Umu...

 

Why (Sonique song)

This article relies largely or entirely on a single source. Relevant discussion may be found on the talk page. Please help improve this article by introducing citations to additional sources.Find sources: Why Sonique song – news · newspapers · books · scholar · JSTOR (April 2021) 2005 single by SoniqueWhySingle by Soniquefrom the album On Kosmo Released30 May 2005 (Germany)GenrePopLength3:15LabelBMGSongwriter(s) Sonique Arndt Roerig Marco Vidovic ...

 

Iskandar Abdul Samad

Malaysian politician In this Malay name, there is no family name. The name Abdul Samad is a patronymic, and the person should be referred to by the given name, Iskandar. Yang Berbahagia Dato' Ir.Iskandar Abdul SamadDPMSإسکندر عبدالصمد‎Exco roles (Selangor)2008–2013Chairman of the Housing, Building Management and Squatters2013–2014Chairman of the Housing, Building Management and Building Settlers2014–2018Chairman of the Housing, Urban Management and Urban LivingFactio...

基金会

基金會圖示 基金會（英語：foundation），也常成為慈善基金會（英語：charitable foundation）是利用自然人、法人或者其他組織捐贈的財產，從事慈善、公益事業的非營利性財團法人（德語：Stiftung）。 法人（德語：Juristische Person）是自然人以外，由法律所創設，得為權利及義務主體的團體。 自法人之組織內容觀察，有以社員的集合為中心者稱為「社團」，有以獨立財產為中心...

 

All That Glitters (American TV series)

US sitcom This article is about the 1977 sitcom. For other uses, see All That Glitters. All That Glitters Screen shot from promotional ad for the series, from Chicago station WFLD Genre Sitcom Soap opera parody Created byNorman LearDirected by James Frawley Herbert Kenwith Theme music composerAlan and Marilyn BergmanOpening themeGenesis Revisited performed by Kenny RankinComposers Ray Brown Bobby Knight Shelly Manne Country of originUnited StatesOriginal languageEnglishNo. of seasons1No. of e...

 

Strategi Solo vs Squad di Free Fire: Cara Menang Mudah!