Project proposals

This page is in Czech, at the moment.

Pokud vás nějaký projekt zaujme a chtěl(a) byste ho zpracovat jako studentskou práci (či jakkoliv jinak se na něm podílet), kontaktujte mě.

Program by umožňoval vizuálně sestavovat formule logiky 1. řádu, čitelně je zobrazovat v textové obarvené podobě (syntax highlighting), nebo ve stromové struktuře. Dále by umožňoval sestavovat a vizualizovat konečné interpretace logiky 1. řádu, rozhodovat platnost formulí v interpretacích a vizualizovat, které podformule jsou/nejsou splněny v dané interpretaci. Program by byl napojený na automatický dokazovač a hledač modelů, a dovedl by například najít a vizualizovat model množiny formulí nebo provést důkaz tvrzení na dokazovači.

Naprostá většina automatických dokazovačů konstruuje důkaz sporem. Pro mnohé aplikace (například konstrukce lemmat) je třeba mít důkaz přímý, kde jsou všechny odvozené klauzule důsledkem axiomů, bez negované domněnky. Cílem práce je napsat konvertor, který by převáděl důkazy sporem na důkazy přímé.

Poznámka: Na této myšlence se již pracuje, viz. SML Proof Manipulation README, bod (3)/a). Kontakt Jasmin Blanchette.

Při důkazu formule (∀x₁)…(∀x_)(∃y)φ lze pomocí Herbrandovy z důkazu odvodit termy, které popisují, jak zkonstruovat y z jednotlivých x_. Cílem práce je napsat program, který bude tyto termy konstruovat, a umožní tak automatické generování objektů (algoritmů) získaných důkazem.

Poznámka: Toto je již z velké části navrženo v Answer Extraction for TPTP implementováno v dokazovači E prover. O to zajímavější by mohlo být tento mechanismus dále využívat ke konstrukci objektů, jako například algoritmů, logických obvodů atd.

Udělat kompilaci různých nástrojů pro automatické dokazování na bootovací live CD založené na Linuxu. Úkol lze dále rozšířit tak, že by CD fungovalo zároveň jako výpočetní uzel, který by se po nastartování připojil do globální výpočetní sítě, např. pomocí VPN nebo P2P mechanismů. V síti by sbíral a řešil od ostatních členů zadané úlohy a naopak jim rozdílel své lokálně zadané úlohy.

Navrhnout databázové prostředí pro algebraické datové typy a implementovat je jako nadstavbu nad rozšířenou open-source relační databází, například Postgre nebo MySQL. Implementace by měla automaticky mapovat ADT na tabulky a mapovat dotazy do SQL jazyka. Data v databázi by se nikdy neměnila, podobně jako v neměnitelných datových strukturách funkcionálních jazyků. Pouze by se vytvářely nové verze jednotlivých záznamů, takže by v databázi existovala kompletní zpětná historie v čase (kterou by samozřejmě bylo možné dle potřeby odmazávat.)

Knihovnu by bylo třeba implementovat v široce rozšířeném jazyce, který má ADT a nebo je umožňuje dosti dobře imitovat. Vhodným jazykem pro by byla např. Scala. Přes JDBC lze pracovat nad téměř jakoukoliv databází. Lze ji integrovat s Javou, která je dnes žádaná.

Poznámka: Funkcionální databáze jako takové existují, ale nemám o tom přehled, nejprve by bylo nutno udělat v tomto směru průzkum existujících technologií.

Pokud vím, neexistuje zatím obfuscator pro Haskell. Cílem práce je takový vytvořit. (Hodil by se mi na vytváření příkladů studentům ).

Budoucnost patří aluminiu¹⁾ distribuovaným decentralizovaným aplikacím. Jak se ukazuje, v mnohých oblastech se v posledních letech prosazují distribuované aplikace na úkor centralizovaných. Nejznámější příklady: P2P file sharing, Distributed revision control systémy (např. Git, Darcs, aj.), distribuované bug tracking systémy či Bitcoin. To se děje ať z důvodů politických (nemožnost kontrolovat konkrétní síť) či praktických (není nutné administrovat často vysoce zatěžovaný server).

V aplikacích tohoto druhu lze úspěšně využít různé zajímavé prvky, jako například funkcionálně reaktivní programování (FRP), multiagentní systémy apod.

Vytvořit klasické fórum bez centrálního serveru. Zprávy by se šířily mezi jednotlivými uživateli formou P2P komunikace. (Trochu podobně funguje Usenet.) Uživatelé by mohli filtrovat příspěvky, které chtějí dostávat, ignorovat konkrétní uživatele (ban), kolektivně hodnotit příspěvky/přispěvatele, atd. Zajímavým prvkem by byla integrace web-of-trust mechanismů.

Vytvořit instant messenger bez centrálního serveru. Aplikace by měla být kompatibilní s Jabber protokolem, a to jednak klientským, aby bylo možné využít stávající klienty, a jednak serverovým, aby bylo možné propojit její P2P síť s Jabber servery a umožnit tak posílání zpráv mezi těmito sítěmi. Například, každý uzel sítě by se mohl chovat jako Jabber server, a P2P vrstva by zajišťovala správné routování zpráv mezi nimi.

Nedávno jsem zjistil, že se touto problematikou už někdo zabývá: XO: XMPP Overlay Service for Distributed Chat.

Pomocí distribuovaných hashovacích tabulek implementujte aplikaci, která bude udržovat globální slovník MD5 hashů z často se objevujících slov. Každý z agentů udržuje po dobu svého spuštění část databáze, případně do ní přispívá. Aplikace umožňuje pomocí slovníku počítat inverzní funkci k nejčastěji se vyskytujícím slovům.

(Toto je tak trochu „hackerská“ aplikace, je otázka, jestli je její přínos spíše pozitivní nebo negativní.)

HTML maily se dnes používají většinou zcela bezúčelně, většinou jsou plné smajlíků, barviček a různých exotických fontů, což pouze snižuje čitelnost a nepřináší to žádnou přidanou hodnotu, spíš naopak. Téma práce nabízí implementovat jedno velmi smysluplné využití: Implementovat filtr, který vezme plaintext email napsaný v LaTeXu a vygeneruje z něj dokument ve formě HTML emailu. K tomu lze využít program program „htlatex“. Tím by si mohli matematici a obecně vědci psát krásně zformátované maily, a adresát by si je mohl číst buďto v LaTeX markupu (pokud je LaTeX fanda) nebo v pěkné grafické podobě. Cílem práce je napsat takový filtr dostatečně obecně, aby to šel použít k různým účelům, například jako automatický SMTP filtr, nebo jako Thunderbird plugin atp.

Při práci na různých projektech je důležité pro programátory (a jiné profese) sledovat množství odvedené práce. To lze provádět sledováním změn souborů v určitých podadresářích a jejich následným vyhodnocením. Na Linuxu tuto možnost poskytuje subsystém Inotify, na Windows existují podobné mechanismy.

Program by bylo možné dále rozšiřovat o další moduly, např. pro sledování síťového provozu (např. dokumentující probíhající SSH komunikaci s pracovním serverem).

Účelem programu by bylo sledovat zvolené události v systému, ukládat zjištěné informace do databáze, a následně umožnit jejich vyhodnocení, například zhodnocení času stráveného programováním určitého projektu za časové období.

Sledování musí být transparentní pro uživatele. Program by neměl být využitelný pro sledování bez vědomí nebo proti vůli uživatele.

JPA (Java Persistence API) knihovny používají dynamické generování kódu za běhu aplikace, kterým vytvářejí třídy pro práci s databází. Tento mechanismus je přitom zcela nešikovný, protože výsledné třídy používají Java reflection (dynamické zkoumání tříd za běhu) a jsou proto pomalé, a náběh aplikace trvá často velmi dlouho. Java překladač přitom podporuje tvorbu kódu během překladu podle anotací. Cílem práce je implementovat JPA (nebo aspoň jeho hlavní část) pomocí této metody.

Velmi často používaná knihovna JasperReport je založená na procedurálním stylu, obtížně se její použití ladí a vyžaduje značnou dávku trpělivosti (z vlastní zkušenosti). Vytvoření podobné knihovny na čistě deklarativní bázi by bylo velkým přínosem.

V případě odcizení notebooku by mohl vhodný program účinně pomoci nalezení pachatele. Po spuštění by se mohl automaticky připojit k internetu a tajně sbírat data a odesílat je na server, například aktuální IP adresu, či natáčet integrovanou web kamerou (kterou mnohé notebooky mají) a mikrofonem okolí.

Zatím bez popisu.

• Detekce jazyka, kódování, … <http://ngramj.sourceforge.net/>
• Možnost automatického lineárního škálování,
• napojení na VCS pro rychlé opravy …