Funktionsprogrammering: Forskelle mellem versioner

I 1980'erne udviklede [[Per Martin-Löf]] den [[intuitionistisk typeteori|intuitionistiske typeteori]] (også kendt som ''konstruktiv typeteori''), hvilket forbandt funktionelle programmer med [[konstruktivt bevis|konstruktive beviser]] af vilkårligt komplekse matematiske udsagn. Disse beviser er udtrykt ved hjælp af ''afhængige typer'' (eng. ''dependent types''). Dette medførte mange nye tilgange til [[automatisk bevisførelse]] og har påvirket udviklingen af flere funktionsprogrammeringssprog.

 

 

== Se også ==