Typechecking is Undecidable when 'Type' is a Type
A function has a dependent type when the type of its result depends upon the value of its argument. The type of all types is the type of every type, including itself. In a typed l-calculus, these two features synergize in a conceptually clean and uniform way to yield enormous expressive power at ve...
| Main Author: | |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149683 |